Problems

The technical problems that the formal methods research community now face are these:

=0in=0in

1.

sep=0in

2.

Verified code We need sound links between specifications, verified algorithms and actual running code. A key goal is to run verified code and formally connect models (algebraic, automata, etc.) to the code.

3.

Sound tools We need to ground a variety of light-weight tools in sound mathematical foundations. Another step that should be investigated soon is a way to guarantee the reliability of decision procedures and enable sharing them as well.

4.

Shared tools and models The labor intensive nature of the work requires that research groups cooperate as much as practical. Since there are a small number of serious efforts in the US, this is possible. The enabling capability is to share libraries of basic mathematical facts. This will also provide sharing of models.

5.

Scalable environments The methodology and tools must be scaled to deal with larger and more complex software systems - verification in the large.

6.

Integrated tools To make the technology useful and acceptable it must be integrated with other tools and with standard programming environments and problem solving environments.

In the future we will face new questions. As formal tools penetrate into software practice and people come to rely on them, the tools will become the objects of intense scrutiny. It must be possible to defend them as ideal instances of reliable, very high assurance software. Our work addresses this issue as well.