Formal Methods Outreach Workshop 2008

A Formal Methods Outreach Workshop was held at SRI International in Menlo Park California during June 9 and 10, 2008. The goal of the meeting was to brainstorm strategies for broadening the uptake of formal methods in education and industry.

1. Formal methods are at a crossroads: On the positive side, the technology is well developed and there are a large number of interesting applications. However, on the negative side, it is no longer considered a part of mainstream computing. There are very few university professors working in the area, sparse course offerings, hardly any flagship projects, and only a small number of graduates.
2. The subject matter of formal methods is both exciting and increasingly relevant. With the dramatic increase in computing power over the last decade, we are now in a position to lift computing to the semantic realm of models and inference. This shift enables a number of novel applications in education and industry. As examples, we can now model both digital and analog hardware, mathematical theories, static and dynamic physical systems, biological networks, complex software systems, and even human psychology and social interactions.
3. Education at all levels can benefit from formal modeling and analysis, and the deeper use of computational metaphors. Currently, computing is taught in terms of low-level information processing tasks whereas the real insights are obtained from the use of computational models and computation. As a simple example, finite automata can serve as a useful metaphor for a number of tasks such as the working of a vending machine, language parsers, or a video game. Interactive games themselves constitute another computational metaphor that is underused in education. Dynamical systems can be used for modeling continuous flows such as moving vehicles, projectiles, fluid levels, speed governors, analog circuits, and pendulums. Hybrid systems combine discrete and continuous state changes and can be used to model thermostats, cruise control systems, and biological and economic systems. As it happens, these computational models can actually be formally analyzed for properties and counterexample scenarios.
4. The industrial uptake of formal methods can also be broadened. Currently, a few industries are both producers and consumers of formal tools. For example, Intel and AMD use such tools for checking circuit equivalence, generating test sequences, model checking finite-state controllers, and proving theorems about floating-point arithmetic algorithms. Microsoft has a number of projects that employ software model checking and automated reasoning to analyze sequential code for termination, assertional correctness, and absence of races and deadlocks. Rockwell-Collins is another leading user of automated reasoning in software verification. Many of the electronic design automation companies like Synopsys, Cadence, and Mentor Graphics sell tools for equivalence and model checking. Matlab recently announced a Simulink design verifier for test case generation and property verification. However, these are still relatively modest efforts compared to the systematic use of formal tools across the entire process. We are not suggesting that the technology is ready for such wider use, but that it is time to contemplate more ambitious and non-traditional applications.
5. Both in education and industry, tools must actively support collaboration. Students learn from doing rather than being told, and from interacting with their peer group at least as much as their teachers. Formal tools should be set up to promote cooperation between different users so that they can share results and exchange criticism.
6. Can we identify projects in different knowledge disciplines that synergistically combine knowledge, deduction, and search to deliver training, insight, and social collaboration in a form that is stimulating and entertaining? As examples, we can ask students to build and experiment with controllers for inverted pendulums, sailing boats, mobile robots, railroad networks, automotives, planes, traffic systems, auctions, ecological systems, gene regulatory networks, and communication networks to achieve skill in formal modeling and algorithmic problem solving. Mathematics itself can benefit from algorithmic ideas if we can teach it as a set of primitives that can be combined to construct algorithmic solutions to problems. Constructive mathematics is a good instance of such an algorithmic approach to mathematics, but the ideas are relevant even when the primitives are not necessarily constructive.

In summary, now is the time to think radical thoughts about new approaches to educational and industrial application of technologies for formal modeling and problem solving.

• Natarajan Shankar, SRI
• Tom Ball, Microsoft Research
• Bob Constable, Cornell University
• Bob Constable's Remarks
• Pat Lincoln, SRI
• Jayadev Misra, University of Texas at Austin
• Draft Report
• Gary Leavens, U. of Central Florida
• Mike Gordon, Cambridge University