GRK 1480:  Programme and Model Analysis

• Subject Area: Computer Science
• Term: from 2008 to 2017
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 47140942

Programme and model analysis is often applied to discover programme errors or certify that a given programme is correct, i.e., complies with its specification. Such a specification may just require that certain errors (like, e.g., null pointer de-referencing) may not occur or make precise assertions concerning resource consumption or the input/output behaviour. In connection with software-intense systems such guaranteed properties play a significant role: The automatic supervision of an intensive care patient must timely respond to a rapid change in the measured values. In an electronic remittance, the money should not only be debited from the bank account of the originator but also be credited onto the account of the recipient. In the best case, a violation of the specification may just incur financial loss. In the worst case, however, it may cause damage for health and integrity of persons.
Currently, there are four competing approaches for programme and model analysis: verification through theorem proving, model checking, abstract interpretation and type systems. Each of these approaches is developed by an international community and has a long history of successes.
Moreover, all four approaches have strong representatives at the universities of Munic. In particular, it is the interplay between the different approaches, which recently has led to novel practical methods. The investigation of such interactions, the development of novel techniques between the poles of the existing ideas and their realisation in practically usable tools is the intended goal of the Research Training Group PUMA. Our vision is the "Verifying Compiler", i.e., the development of methods and tools, which allow for a piece of software or a software model to guarantee with the same ease properties as a compiler allows to generate code.

• DFG Programme: Research Training Groups
• Applicant Institution: Technische Universität München (TUM)
• Co-Applicant Institution: Ludwig-Maximilians-Universität München
• Spokesperson: Professor Dr. Helmut Seidl
• Participating Researchers: Professor Dr. Javier Esparza; Professor Dr. Martin Hofmann (†); Professor Dr.-Ing. Alois Knoll; Professor Tobias Nipkow, Ph.D.; Professor Dr. Andrey Rybalchenko; Professorin Dr.-Ing. Birgit Vogel-Heuser