With recent developments of modern theorem provers, the completely formal development of software is gradually becoming feasible. The aim of the AWE project is to increase this feasibility by developing a methodology for the reuse of formal developments under the slogan ``Abstraction for Reuse'': given a formal development we want to make it more abstract to be able to reuse it in many different, similar situations. This way, the effort of formal development can be reused, and hence gets reduced each time.

The project focusses on foundations in formal logic and developing tool support, using Isabelle as the implementation basis and theorem proving engine. The project has been supported by the German research council DFG from 2002 to 2008.

This Web Site

This site has been set up to disseminate the project results, and contains the following:

Latest Project News