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.
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}
}
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}
}
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}
}
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}
}
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}
}
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}
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}
}
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}
}
Dokument aufrufenJ. Haltermann, M. Jakobs, C. Richter, und H. Wehrheim, "Parallel Program Analysis via Range Splitting" in Proc. FASE, 2023.