## 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.