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, M. Jakobs, C. Richter, und H. Wehrheim, "Parallel Program Analysis via Range Splitting" in Proc. FASE, 2023.
    doi: 10.1007/978-3-031-30826-0_11
    @inproceedings{DBLP:conf/fase/HaltermannJRW23,
      author = {Jan Haltermann and Marie Jakobs and Cedric Richter and Heike Wehrheim},
      editor = {Leen Lambers and Sebasti{\'{a}}n Uchitel},
      title = {Parallel Program Analysis via Range Splitting},
      booktitle = { {FASE} },
      series = {LNCS},
      volume = {13991},
      pages = {195--219},
      publisher = {Springer},
      year = {2023},
      url = {https://doi.org/10.1007/978-3-031-30826-0\_11},
      doi = {10.1007/978-3-031-30826-0\_11},
      timestamp = {Sat, 13 May 2023 01:07:19 +0200},
      biburl = {https://dblp.org/rec/conf/fase/HaltermannJRW23.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    D. Beyer, J. Haltermann, T. Lemberger, und H. Wehrheim, "Decomposing Software Verification into Off-the-Shelf Components: An Application to CEGAR" in Proc. ICSE, 2022.
    doi: 10.1145/3510003.3510064
    @inproceedings{DBLP:conf/icse/00010HW22,
      author = {Dirk Beyer and Jan Haltermann and Thomas Lemberger and Heike Wehrheim},
      title = {Decomposing Software Verification into Off-the-Shelf Components: An Application to {CEGAR}},
      booktitle = { {ICSE} },
      pages = {536--548},
      publisher = {{ACM}},
      year = {2022},
      url = {https://doi.org/10.1145/3510003.3510064},
      doi = {10.1145/3510003.3510064},
      timestamp = {Fri, 02 Dec 2022 14:14:00 +0100},
      biburl = {https://dblp.org/rec/conf/icse/00010HW22.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    J. Haltermann und H. Wehrheim, "Machine Learning Based Invariant Generation: A Framework and Reproducibility Study" in Proc. ICST, 2022.
    doi: 10.1109/ICST53961.2022.00012
    @inproceedings{DBLP:conf/icst/HaltermannW22,
      author = {Jan Haltermann and Heike Wehrheim},
      title = {Machine Learning Based Invariant Generation: {A} Framework and Reproducibility Study},
      booktitle = { {ICST}},
      pages = {12--23},
      publisher = {{IEEE}},
      year = {2022},
      url = {https://doi.org/10.1109/ICST53961.2022.00012},
      doi = {10.1109/ICST53961.2022.00012},
      timestamp = {Mon, 13 Jun 2022 16:53:37 +0200},
      biburl = {https://dblp.org/rec/conf/icst/HaltermannW22.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    J. Haltermann und H. Wehrheim, "Information Exchange Between Over- and Underapproximating Software Analyses" in Proc. SEFM, 2022.
    doi: 10.1007/978-3-031-17108-6_3
    @inproceedings{DBLP:conf/sefm/HaltermannW22,
      author = {Jan Haltermann and Heike Wehrheim},
      editor = {Bernd{-}Holger Schlingloff and Ming Chai},
      title = {Information Exchange Between Over- and Underapproximating Software Analyses},
      booktitle = { {SEFM} },
      series = {LNCS},
      volume = {13550},
      pages = {37--54},
      publisher = {Springer},
      year = {2022},
      url = {https://doi.org/10.1007/978-3-031-17108-6\_3},
      doi = {10.1007/978-3-031-17108-6\_3},
      timestamp = {Tue, 18 Oct 2022 22:16:55 +0200},
      biburl = {https://dblp.org/rec/conf/sefm/HaltermannW22.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    J. Haltermann und H. Wehrheim, "CoVEGI: Cooperative Verification via Externally Generated Invariants" in Proc. FASE, 2021.
    doi: 10.1007/978-3-030-71500-7_6
    @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 = { {FASE} },
      series = {LNCS},
      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. Jakobs und C. Richter, "CoVeriTest with Adaptive Time Scheduling (Competition Contribution)" in Proc. FASE, 2021.
    doi: 10.1007/978-3-030-71500-7_18
    @inproceedings{DBLP:conf/fase/JakobsR21,
      author = {Marie Jakobs and Cedric Richter},
      editor = {Esther Guerra and Mari{\"{e}}lle Stoelinga},
      title = {CoVeriTest with Adaptive Time Scheduling (Competition Contribution)},
      booktitle = { {FASE} },
      series = {LNCS},
      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. ASE, 2020.
    doi: 10.1145/3324884.3416633
    @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 = { {ASE} },
      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. ISoLA, 2020.
    doi: 10.1007/978-3-030-61362-4_8
    @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 = { {ISoLA}},
      series = {LNCS},
      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. Jakobs, "CoVeriTest: Cooperative Verifier-Based Testing" in Proc. FASE, 2019.
    doi: 10.1007/978-3-030-16722-6_23
    @inproceedings{DBLP:conf/fase/BeyerJ19,
      author = {Dirk Beyer and Marie Jakobs},
      editor = {Reiner H{\"{a}}hnle and Wil M. P. van der Aalst},
      title = {CoVeriTest: Cooperative Verifier-Based Testing},
      booktitle = { {FASE} },
      series = {LNCS},
      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. Jakobs, "CoVeriTest: Cooperative Verifier-Based Testing" in Proc. FASE, 2019.
    doi: 10.1007/978-3-030-16722-6_23
    @inproceedings{DBLP:conf/fase/BeyerJ19,
      author = {Dirk Beyer and Marie Jakobs},
      editor = {Reiner H{\"{a}}hnle and Wil M. P. van der Aalst},
      title = {CoVeriTest: Cooperative Verifier-Based Testing},
      booktitle = { {FASE} },
      series = {LNCS},
      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. Jakobs, T. Lemberger, und H. Wehrheim, "Reducer-based construction of conditional verifiers" in Proc. ICSE, 2018.
    doi: 10.1145/3180155.3180259
    @inproceedings{DBLP:conf/icse/BeyerJLW18,
      author = {Dirk Beyer and Marie 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 = { {ICSE} },
      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: 19.01.2024)  | 
Zum Seitananfang scrollen Scroll to the top of the page