Achtung:

Sie haben Javascript deaktiviert!
Sie haben versucht eine Funktion zu nutzen, die nur mit Javascript möglich ist. Um sämtliche Funktionalitäten unserer Internetseite zu nutzen, aktivieren Sie bitte Javascript in Ihrem Browser.

Jan Haltermann, Manuel Töws, Felix Pauck, Cedric Richter, Heike Wehrheim, Jürgen König, Arnab Sharma, Steffen Beringer, Oleksandra Koslova, Elisabeth Schlatt (left to right) Show image information

Jan Haltermann, Manuel Töws, Felix Pauck, Cedric Richter, Heike Wehrheim, Jürgen König, Arnab Sharma, Steffen Beringer, Oleksandra Koslova, Elisabeth Schlatt (left to right)

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


Open list in Research Information System

Reducer-Based Construction of Conditional Verifiers

D. Beyer, M. Jakobs, T. Lemberger, H. Wehrheim, in: Proceedings of the 40th International Conference on Software Engineering (ICSE), ACM, 2018, pp. 1182--1193

to appear


    CoVeriTest: Cooperative Verifier-Based Testing

    D. Beyer, M. Jakobs, in: Fundamental Approaches to Software Engineering, 2019


    Cooperative Verification via Collective Invariant Generation

    J.F. Haltermann, H. Wehrheim, in: arXiv:2008.04551, 2020

    Software verification has recently made enormous progress due to the development of novel verification methods and the speed-up of supporting technologies like SMT solving. To keep software verification tools up to date with these advances, tool developers keep on integrating newly designed methods into their tools, almost exclusively by re-implementing the method within their own framework. While this allows for a conceptual re-use of methods, it requires novel implementations for every new technique. In this paper, we employ cooperative verification in order to avoid reimplementation and enable usage of novel tools as black-box components in verification. Specifically, cooperation is employed for the core ingredient of software verification which is invariant generation. Finding an adequate loop invariant is key to the success of a verification run. Our framework named CoVerCIG allows a master verification tool to delegate the task of invariant generation to one or several specialized helper invariant generators. Their results are then utilized within the verification run of the master verifier, allowing in particular for crosschecking the validity of the invariant. We experimentally evaluate our framework on an instance with two masters and three different invariant generators using a number of benchmarks from SV-COMP 2020. The experiments show that the use of CoVerCIG can increase the number of correctly verified tasks without increasing the used resources


      Open list in Research Information System

      Contact

      Prof. Dr. Heike Wehrheim

      Specification and Modelling of Software Systems

      Heike Wehrheim
      Phone:
      +49 5251 60-4331
      Office:
      O4.225

      Jan Haltermann, M.Sc.

      Specification and Modelling of Software Systems

      Jan  Haltermann
      Phone:
      +49 5251 60-1709
      Fax:
      +49 5251 60-3993
      Office:
      O4.131

      Office hours:

      Availability (Working hours):
      Monday - Friday
      08:30 am until 15:30 pm

      Calender

      The University for the Information Society