Cooperative Software Verification

Teilnehmende:

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

Förderung:

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

Cooperative Software Verification

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.

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.

Publikationen

  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    J. Haltermann und H. Wehrheim, "CoVEGI: Cooperative Verification via Externally Generated Invariants" in Proc. Fundamental Approaches to Software Engineering - 24th International Conference, FASE 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, 2021, pp. 108-129.
    @inproceedings{DBLP:conf/fase/HaltermannW21,
      author = {Jan Haltermann and Heike Wehrheim},
      editor = {Esther Guerra and Mari{\"{e}}lle Stoelinga},
      title = {CoVEGI: Cooperative Verification via Externally Generated Invariants},
      booktitle = {Fundamental Approaches to Software Engineering - 24th International Conference, {FASE} 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings},
      series = {Lecture Notes in Computer Science},
      volume = {12649},
      pages = {108--129},
      publisher = {Springer},
      year = {2021},
      url = {https://doi.org/10.1007/978-3-030-71500-7\_6},
      doi = {10.1007/978-3-030-71500-7\_6},
      timestamp = {Fri, 14 May 2021 08:34:15 +0200},
      biburl = {https://dblp.org/rec/conf/fase/HaltermannW21.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    M. - und C. Richter, "CoVeriTest with Adaptive Time Scheduling (Competition Contribution)" in Proc. Fundamental Approaches to Software Engineering - 24th International Conference, FASE 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, 2021, pp. 358-362.
    @inproceedings{DBLP:conf/fase/JakobsR21,
      author = {Marie{-}Christine Jakobs and Cedric Richter},
      editor = {Esther Guerra and Mari{\"{e}}lle Stoelinga},
      title = {CoVeriTest with Adaptive Time Scheduling (Competition Contribution)},
      booktitle = {Fundamental Approaches to Software Engineering - 24th International Conference, {FASE} 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings},
      series = {Lecture Notes in Computer Science},
      volume = {12649},
      pages = {358--362},
      publisher = {Springer},
      year = {2021},
      url = {https://doi.org/10.1007/978-3-030-71500-7\_18},
      doi = {10.1007/978-3-030-71500-7\_18},
      timestamp = {Fri, 14 May 2021 08:34:15 +0200},
      biburl = {https://dblp.org/rec/conf/fase/JakobsR21.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    C. Richter und H. Wehrheim, "Attend and Represent: A Novel View on Algorithm Selection for Software Verification" in Proc. 35th IEEE/ACM International Conference on Automated Software Engineering, ASE 2020, Melbourne, Australia, September 21-25, 2020, 2020, pp. 1016-1028.
    @inproceedings{DBLP:conf/kbse/RichterW20,
      author = {Cedric Richter and Heike Wehrheim},
      title = {Attend and Represent: {A} Novel View on Algorithm Selection for Software Verification},
      booktitle = {35th {IEEE/ACM} International Conference on Automated Software Engineering, {ASE} 2020, Melbourne, Australia, September 21-25, 2020},
      pages = {1016--1028},
      publisher = {{IEEE}},
      year = {2020},
      url = {https://doi.org/10.1145/3324884.3416633},
      doi = {10.1145/3324884.3416633},
      timestamp = {Fri, 12 Feb 2021 13:04:43 +0100},
      biburl = {https://dblp.org/rec/conf/kbse/RichterW20.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org}
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    D. Beyer und H. Wehrheim, "Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework" in Proc. 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, 2020, pp. 143-167.
    @inproceedings{DBLP:conf/isola/0001W20,
      author = {Dirk Beyer and Heike Wehrheim},
      editor = {Tiziana Margaria and Bernhard Steffen},
      title = {Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework},
      booktitle = {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}},
      series = {Lecture Notes in Computer Science},
      volume = {12476},
      pages = {143--167},
      publisher = {Springer},
      year = {2020},
      url = {https://doi.org/10.1007/978-3-030-61362-4\_8},
      doi = {10.1007/978-3-030-61362-4\_8},
      timestamp = {Fri, 14 May 2021 08:34:11 +0200},
      biburl = {https://dblp.org/rec/conf/isola/0001W20.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    D. Beyer und M. -, "CoVeriTest: Cooperative Verifier-Based Testing" in Proc. Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, 2019, pp. 389-408.
    @inproceedings{DBLP:conf/fase/BeyerJ19,
      author = {Dirk Beyer and Marie{-}Christine Jakobs},
      editor = {Reiner H{\"{a}}hnle and Wil M. P. van der Aalst},
      title = {CoVeriTest: Cooperative Verifier-Based Testing},
      booktitle = {Fundamental Approaches to Software Engineering - 22nd International Conference, {FASE} 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings},
      series = {Lecture Notes in Computer Science},
      volume = {11424},
      pages = {389--408},
      publisher = {Springer},
      year = {2019},
      url = {https://doi.org/10.1007/978-3-030-16722-6\_23},
      doi = {10.1007/978-3-030-16722-6\_23},
      timestamp = {Tue, 29 Dec 2020 18:33:00 +0100},
      biburl = {https://dblp.org/rec/conf/fase/BeyerJ19.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    D. Beyer und M. -, "CoVeriTest: Cooperative Verifier-Based Testing" in Proc. Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, 2019, pp. 389-408.
    @inproceedings{DBLP:conf/fase/BeyerJ19,
      author = {Dirk Beyer and Marie{-}Christine Jakobs},
      editor = {Reiner H{\"{a}}hnle and Wil M. P. van der Aalst},
      title = {CoVeriTest: Cooperative Verifier-Based Testing},
      booktitle = {Fundamental Approaches to Software Engineering - 22nd International Conference, {FASE} 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings},
      series = {Lecture Notes in Computer Science},
      volume = {11424},
      pages = {389--408},
      publisher = {Springer},
      year = {2019},
      url = {https://doi.org/10.1007/978-3-030-16722-6\_23},
      doi = {10.1007/978-3-030-16722-6\_23},
      timestamp = {Tue, 29 Dec 2020 18:33:00 +0100},
      biburl = {https://dblp.org/rec/conf/fase/BeyerJ19.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    D. Beyer, M. -, T. Lemberger, und H. Wehrheim, "Reducer-based construction of conditional verifiers" in Proc. Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, May 27 - June 03, 2018, 2018, pp. 1182-1193.
    @inproceedings{DBLP:conf/icse/BeyerJLW18,
      author = {Dirk Beyer and Marie{-}Christine Jakobs and Thomas Lemberger and Heike Wehrheim},
      editor = {Michel Chaudron and Ivica Crnkovic and Marsha Chechik and Mark Harman},
      title = {Reducer-based construction of conditional verifiers},
      booktitle = {Proceedings of the 40th International Conference on Software Engineering, {ICSE} 2018, Gothenburg, Sweden, May 27 - June 03, 2018},
      pages = {1182--1193},
      publisher = {{ACM}},
      year = {2018},
      url = {https://doi.org/10.1145/3180155.3180259},
      doi = {10.1145/3180155.3180259},
      timestamp = {Tue, 10 Aug 2021 14:29:45 +0200},
      biburl = {https://dblp.org/rec/conf/icse/BeyerJLW18.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
(Stand: 23.09.2021)