In the last years, four competing approaches for program and model analysis have been developed: verification through theorem proving, model checking, abstract interpretation and via type systems. The Munich universities hosting the program have expert researchers in all of these areas. Our goal is to stimulate cross-fertilization between these approaches resulting in a better understanding of their common basis and their distinctive properties, and leading to better algorithms and tools. Our vision is the Verifying Compiler, i.e., the development of methods and tools that examine not only whether a program or model is syntactically correct, but also whether it behaves according to its specification. Test applications are planned in the area of software-intensive systems.
Sub-Projects of PUMA
In the first period of funding, research has essentially been performed within the following five projects. Each project integrated ideas and methods from several of the approaches.
- Combination of Methods
- Certified Analyses
- Falsifying Analyses
- Quantitative Analyses
- Software-intensive Systems
In the next period, we plan to develop these sub-projects further by slightly shifting the focus onto fundamental approaches. Also, the application area will be focused onto autonomous systems. The new sub-projects are the following: