Background
The development of correct programs is one of the core problems of computer science. A multitude of techniques has been developed to this end, collectively known as formal methods, which allow to prove the correctness of a program with respect to a specification (verification) or to stepwise formally develop a correct program from a specification.
Unfortunately, verification and formal development require a large amount of proof work, which until now has hampered their deployment in industrial practice. The proofs in question are for the most part not very sophisticated mathematically, but long and numerous, and hence error-prone. Without the possibility to check their correctness by machine, correctness cannot be guaranteed, which indeed is the whole point of formal methods.
To automatically check and develop proofs, a number of theorem provers have been developed. In the last ten years, progress in this area has come in leaps and bounds: in particular, so called higher-order provers (based in higher-order logic), such as Coq, PVS or Isabelle have reached a level of maturity, where they support the formalisation of whole textbooks, or even attack open mathematical problems. It is just a matter of time when theorem provers will be able to support the formal development of realistic software, and formal development and verification will become part of the industrial practice, at least for safety or mission critical software. There already are examples of substantial formal verification in industry, such as the verification of the Pentium microprocessors by Intel.
With the foundations being laid and sufficient tool support available, questions of good practice and appropriate user interfaces become more important. In formal stepwise development, instead of proving each new development step after the fact (``invent&verify''), it seems advantageous to use a library of transformation rules, which have been shown correct once and for all. Transformation rules can be considered as the formal counterparts of the well-known design patterns: they reduce the proof work and guide the development. The question is, where do we get transformation rules from?
Project Aims
This is where the AWE project starts. The focus of AWE is the development of a methodology, which allows the systematic, gradual generalisation of a formal development. Thus, new transformation rules can be derived by generalsing given, prototypical developments. We call this abstraction for reuse: abstract a given development now to enable reuse later. This way, the whole of the development process is reused, which is more powerful than merely reusing the product (e.g. reusing single modules or proofs).
A cornerstone of the project is the implementation of the developed concepts on the basis of the modern theorem prover Isabelle, with particular consideration of genericity: concepts for reuse and abstraction should not only be considered for one particular formal method, but be applicable across a wide variety of formal methods.
If you read German, the report on the first phase of the project can be found here.
Results
This is a short overview of the main results of the project:- We have development a technique to systematically generalise natural deductions in a logical framework setting, and implemented this in Isabelle (see our TPHOLs 04 paper).
- We have extended Isabelle with signature and theory morphisms, which allows us to model parameterised theories and transformation rules (see our NJC'06 paper).
- We have formalised several well-known transformation rules in Isabelle, and examplary shown how to derive new rules (see this paper, or our NJC'03 paper).
- In cooperation with David Aspinall, we have developed a new framework for user interfaces, subsuming previous work in Proof General and graphical user interfaces such as TAS and IsaWin (see our UITP'03 paper, or this paper).
History
The first phase of the project has been granted funding in July 2000, and the project started in January 2002. The first phase of the project ran until May 2004. The second (and final) phase of the project has been granted funding in November 2005, and started in March 2006, running for two years.
The principal researcher is Dr. Christoph Lüth, who together with Prof. Bernd Krieg-Brückner started the project. Initially, Dr. Einar Broch Johnsen was employed as research assistant, but he left to take up an assistant professorship at Oslo University. In his place, Maksym Bortin joined the AWE team, as a research assistant and graduate student working on his PhD.
About the Project Name
AWE is a German acronym for Abstraktion und Wiederverwendung formaler Entwicklungen (abstraction and reuse of formal developments); the pun (such as it is) is, of course, intentional.
However, the name goes back to the last century, and in the light of more recent events, we would like to stress that we do not indent to shock anyone, other than by the brilliance of our research. Further, we do not sell nuclear warheads; for that, you would be looking for a different AWE.