Software Verification

The aim of software verification is the assurance of high quality software, in particular absence of unintended and erroneous behaviour. Today, a range of different tools provide software analysis techniques, covering the whole area from static and dynamic analysis to model checking. All of these techniques have their individual strengths and weaknesses.

Participants: Heike Wehrheim, Jan Haltermann, Dirk Beyer (LMU Munich), Thomas Lemberger (LMU Munich)

Cooperative Software Verification

The goal of this research project is the enhancement of precision and performance in software verification by cooperation between different verification tools and techniques.

Cooperative software verification requires (1) to enable exchange of information between verification tools and sound usage of such information, and (2) to learn how and when to cooperate. Cooperation targets the division of labour as to have every technology work on the tasks it is best at, but also aims at the increase of trust in the soundness of the analysis by having tools mutually check their results. The objective of our project is the development of a practical methodology of cooperative software verification based on a provably sound theory of cooperation. Our methodology targets safety verification.

Funding

This project is funded by the German Research Council DFG (Cooperative Software Verification , 2019 - 2022).

Publications

Reducer-Based Construction of Conditional Verifiers
D. Beyer, M.-C. Jakobs, T. Lemberger, H. Wehrheim, in: Proceedings of the 40th International Conference on Software Engineering (ICSE), ACM, 2018, pp. 1182--1193.
CoVeriTest: Cooperative Verifier-Based Testing
D. Beyer, M.-C. Jakobs, in: Fundamental Approaches to Software Engineering, Cham, 2019.
Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework
D. Beyer, H. Wehrheim, in: T. Margaria, B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part {I}, Springer, 2020, pp. 143–167.
Cooperative Verification via Collective Invariant Generation
J.F. Haltermann, H. Wehrheim, ArXiv:2008.04551 (2020).
Show all publications