This project is funded by the German Research Council DFG (Cooperative Software Verification , 2019 - 2022, 2024 – 2027).
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 und H. Wehrheim, "Exchanging information in cooperative software validation" Software and Systems Modeling.
doi: 10.1007/s10270-024-01155-3
@article{GIA_Journal,
author={Jan Haltermann and Heike Wehrheim},
title = {Exchanging information in cooperative software validation},
journal = {Software and Systems Modeling},
year = {2024},
doi = {10.1007/s10270-024-01155-3}
}
J. Haltermann, M. Jakobs, C. Richter, und H. Wehrheim, "Parallel Program Analysis on Path Ranges" CoRR, vol. abs/2402.11938.
doi: 10.48550/ARXIV.2402.11938
@article{DBLP:journals/corr/abs-2402-11938,
author = {Jan Haltermann and MarieChristine Jakobs and Cedric Richter and Heike Wehrheim},
title = {Parallel Program Analysis on Path Ranges},
journal = {CoRR},
volume = {abs/2402.11938},
year = {2024},
url = {https://doi.org/10.48550/arXiv.2402.11938},
doi = {10.48550/ARXIV.2402.11938},
eprinttype = {arXiv},
eprint = {2402.11938},
timestamp = {Thu, 21 Mar 2024 15:46:29 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2402-11938.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
J. Haltermann, M. -, C. Richter, und H. Wehrheim, "Ranged Program Analysis: A Parallel Divide-and-Conquer Approach for Software Verification" in Proc. Software Engineering 2024, Fachtagung des GI-Fachbereichs Softwaretechnik, Linz, Austria, February 26 - March 1, 2024, 2024.
doi: 10.18420/SW2024_52
@inproceedings{DBLP:conf/se/HaltermannJRW24,
author = {Jan Haltermann and Marie{-}Christine Jakobs and Cedric Richter and Heike Wehrheim},
editor = {Rick Rabiser and Manuel Wimmer and Iris Groher and Andreas Wortmann and Bianca Wiesmayr},
title = {Ranged Program Analysis: {A} Parallel Divide-and-Conquer Approach for Software Verification},
booktitle = {Software Engineering 2024, Fachtagung des GI-Fachbereichs Softwaretechnik, Linz, Austria, February 26 - March 1, 2024},
series = {{LNI}},
volume = {{P-343}},
pages = {157--158},
publisher = {Gesellschaft f{\"{u}}r Informatik e.V.},
year = {2024},
url = {https://doi.org/10.18420/sw2024\_52},
doi = {10.18420/SW2024\_52},
timestamp = {Mon, 11 Mar 2024 16:51:10 +0100},
biburl = {https://dblp.org/rec/conf/se/HaltermannJRW24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
M. Chalupa und C. Richter, "Bubaak-SpLit: Split what you cannot verify (Competition contribution)" in Proc. Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III, 2024.
doi: 10.1007/978-3-031-57256-2_20
@inproceedings{DBLP:conf/tacas/ChalupaR24,
author = {Marek Chalupa and Cedric Richter},
editor = {Bernd Finkbeiner and Laura Kov{\'{a}}cs},
title = {Bubaak-SpLit: Split what you cannot verify (Competition contribution)},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, {TACAS} 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part {III}},
series = {Lecture Notes in Computer Science},
volume = {14572},
pages = {353--358},
publisher = {Springer},
year = {2024},
url = {https://doi.org/10.1007/978-3-031-57256-2\_20},
doi = {10.1007/978-3-031-57256-2\_20},
timestamp = {Sat, 08 Jun 2024 13:13:56 +0200},
biburl = {https://dblp.org/rec/conf/tacas/ChalupaR24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
D. Beyer, M. Kettl, und T. Lemberger, "Fault Localization on Verification Witnesses" in Proc. Proceedings of the 30th International Symposium on Model Checking Software (SPIN~2024, Luxembourg City, Luxembourg, April 10-11), 2024.
@inproceedings{SPIN24a,
author = {Dirk Beyer and Matthias Kettl and Thomas Lemberger},
title = {Fault Localization on Verification Witnesses},
booktitle = {Proceedings of the 30th International Symposium on Model Checking Software (SPIN~2024, Luxembourg City, Luxembourg, April 10-11)},
pages = {},
year = {2024},
series = {LNCS},
publisher = {Springer},
pdf = {https://sosy-lab.org/research/pub/2024-SPIN.Fault_Localization_on_Verification_Witnesses.pdf},
abstract = {When verifiers report an alarm, they export a violation witness (exchangeable counterexample) that helps validate the reachability of that alarm. Conventional wisdom says that this violation witness should be very precise: the ideal witness describes a single error path for the validator to check. But we claim that verifiers overshoot and produce large witnesses with information that makes validation unnecessarily difficult. To check our hypothesis, we reduce violation witnesses to that information that automated fault-localization approaches deem relevant for triggering the reported alarm in the program. We perform a large experimental evaluation on the witnesses produced in the International Competition on Software Verification (SV-COMP 2023). It shows that our reduction shrinks the witnesses considerably and enables the confirmation of verification results that were not confirmable before.},
keyword = {Software Model Checking, Witness-Based Validation, CPAchecker},
annote = {Nominated for best paper. This work was also presented with a poster at the 46th International Conference on Software Engineering (ICSE 2024, Lisbon, Portugal, April 14-20): Extended Abstract.},
artifact = {10.5281/zenodo.10794627},
doinone = {TBD},
funding = {DFG-CONVEY,DFG-IDEFIX,DFG-COOP},
}
D. Baier, D. Beyer, P. Chien, M. Jakobs, M. Jankola, M. Kettl, N. Lee, T. Lemberger, M. Lingsch-Rosenfeld, H. Wachowitz, und P. Wendler, "Software Verification with CPAchecker 3.0: Tutorial and User Guide" in Proc. Proc. FM, 2024.
@inproceedings{FM24a,
author = {Daniel Baier and Dirk Beyer and Po-Chun Chien and Marie-Christine Jakobs and Marek Jankola and Matthias Kettl and Nian-Ze Lee and Thomas Lemberger and Marian Lingsch-Rosenfeld and Henrik Wachowitz and Philipp Wendler},
title = {Software Verification with {CPAchecker} 3.0: {Tutorial} and User Guide},
booktitle = {Proc.\ FM},
pages = {},
year = {2024},
series = {LNCS~},
publisher = {Springer},
url = {https://cpachecker.sosy-lab.org},
pdf = {https://www.sosy-lab.org/research/pub/2024-FM.Software_Verification_with_CPAchecker_3.0_Tutorial_and_User_Guide.pdf},
presentation = {},
abstract = {This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking, Impact, interpolation-based model checking, k-induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases for CPAchecker in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. An extended version also shows further use cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 3.0. This user guide's latest version and other documentation are available at https://cpachecker.sosy-lab.org/doc.php.},
keyword = {CPAchecker, Software Model Checking, Software Testing},
annote = {},
artifact = {10.5281/zenodo.12666378},
doinone = {Unpublished: Last checked: 2024-07-08},
funding = {DFG-COOP, DFG-CONVEY, DFG-IDEFIX},
}
D. Beyer, M. Kettl, und T. Lemberger, "Decomposing Software Verification Using Distributed Summary Synthesis" Proc. ACM Softw. Eng. vol. 1, iss. FSE.
doi: 10.1145/3660766
@article{DSS-PACMSE,
author = {Dirk Beyer and Matthias Kettl and Thomas Lemberger},
title = {Decomposing Software Verification Using Distributed Summary Synthesis},
journal = {Proc. ACM Softw. Eng.},
volume = {1},
number = {FSE},
year = {2024},
publisher = {ACM},
doi = {10.1145/3660766},
url = {https://www.sosy-lab.org/research/distributed-summary-synthesis/},
pdf = {https://www.sosy-lab.org/research/pub/2024-FSE.Decomposing_Software_Verification_using_Distributed_Summary_Synthesis.pdf},
presentation = {},
keyword = {CPAchecker,Software Model Checking},
articleno = {90},
artifact = {10.5281/zenodo.11095864},
funding = {DFG-CONVEY,DFG-COOP},
issue_date = {July 2024},
numpages = {23},
}
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}
}
J. Haltermann, M. -, C. Richter, und H. Wehrheim, "Ranged Program Analysis via Instrumentation" in Proc. Software Engineering and Formal Methods - 21st International Conference, SEFM 2023, Eindhoven, The Netherlands, November 6-10, 2023, Proceedings, 2023.
doi: 10.1007/978-3-031-47115-5_9
@inproceedings{DBLP:conf/sefm/HaltermannJRW23,
author = {Jan Haltermann and Marie{-}Christine Jakobs and Cedric Richter and Heike Wehrheim},
editor = {Carla Ferreira and Tim A. C. Willemse},
title = {Ranged Program Analysis via Instrumentation},
booktitle = {Software Engineering and Formal Methods - 21st International Conference, {SEFM} 2023, Eindhoven, The Netherlands, November 6-10, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14323},
pages = {145--164},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-47115-5\_9},
doi = {10.1007/978-3-031-47115-5\_9},
timestamp = {Tue, 28 Nov 2023 20:06:05 +0100},
biburl = {https://dblp.org/rec/conf/sefm/HaltermannJRW23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
D. Beyer, S. Kanav, und H. Wachowitz, "CoVeriTeam Service: Verification as a Service" in Proc. Proc. ICSE, 2023.
doi: 10.1109/ICSE-Companion58688.2023.00017
@inproceedings{ICSE23,
author = {Dirk Beyer and Sudeep Kanav and Henrik Wachowitz},
title = {{CoVeriTeam} Service: Verification as a Service},
booktitle = {Proc.\ ICSE},
pages = {21-25},
year = {2023},
publisher = {IEEE},
doi = {10.1109/ICSE-Companion58688.2023.00017},
url = {https://coveriteam-service.sosy-lab.org/static/index.html},
pdf = {https://www.sosy-lab.org/research/pub/2023-ICSE.CoVeriTeam_Service_Verification_as_a_Service.pdf},
abstract = {The research community has developed numerous tools for solving verification problems, but we are missing a common interface for executing them. This means users have to spend considerable effort on the installation and parameter setup, for each new tool (version) they want to execute. The situation could make a verification researcher wanting to experiment with a new verification tool turn away from it. We aim to make it easier for users to execute verification tools, as well as provide mechanism for tool developers to make their tools easily accessible. Our solution combines a web service and a common interface for verification tools. The presented service has been used during the 2023 competitions on software verification and testing, for integration testing. As another use- case, we developed a service for incremental verification on top of the {CoVeriTeam} Service and demonstrate its use in a continuous-integration process.},
keyword = {Software Model Checking,Incremental Verification,Cooperative Verification},
_sha256 = {604dd391b6a49e46e97b6faafbb3cc331ccf5c04e3d364cf1e76a2c99c1c267f},
artifact = {10.5281/zenodo.7276532},
funding = {DFG-CONVEY,DFG-COOP},
}
D. Beyer, "Competition on Software Verification and Witness Validation: SV-COMP 2023" in Proc. Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2023, Paris, France, April 22-27), 2023.
doi: 10.1007/978-3-031-30820-8_29
@inproceedings{TACAS23b,
author = {Dirk Beyer},
title = {Competition on Software Verification and Witness Validation: {SV-COMP 2023}},
booktitle = {Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2023, Paris, France, April 22-27)},
editor = {S. Sankaranarayanan and N. Sharygina},
pages = {495--522},
year = {2023},
series = {LNCS~13994},
publisher = {Springer},
doi = {10.1007/978-3-031-30820-8_29},
sha256 = {1d35ae38d4e87c267ccc34cba880994b6f6a7927491ec13ba3cc548a29e81e5c},
url = {https://sv-comp.sosy-lab.org/2023/},
keyword = {Competition on Software Verification (SV-COMP),Competition on Software Verification (SV-COMP Report),Software Model Checking},
_pdf = {https://www.sosy-lab.org/research/pub/2023-TACAS.Competition_on_Software_Verification_and_Witness_Validation_SV-COMP_2023.pdf},
funding = {DFG-COOP},
}
D. Beyer, "Software Testing: 5th Comparative Evaluation: Test-Comp 2023" in Proc. Proceedings of the 26th International Conference on Fundamental Approaches to Software Engineering (FASE~2023, Paris, France, April 22-27), 2023.
doi: 10.1007/978-3-031-30826-0_17
@inproceedings{FASE23,
author = {Dirk Beyer},
title = {Software Testing: 5th Comparative Evaluation: {Test-Comp 2023}},
booktitle = {Proceedings of the 26th International Conference on Fundamental Approaches to Software Engineering (FASE~2023, Paris, France, April 22-27)},
editor = {L. Lambers and S. Uchitel},
pages = {309--323},
year = {2023},
series = {LNCS~13991},
publisher = {Springer},
isbn = {},
doi = {10.1007/978-3-031-30826-0_17},
sha256 = {7110c26bf3c9311f84346a108a59318687bdadde4879f83d047f1a0fc546b630},
url = {https://test-comp.sosy-lab.org/2023/},
keyword = {Competition on Software Testing (Test-Comp),Competition on Software Testing (Test-Comp Report),Software Testing},
_pdf = {https://www.sosy-lab.org/research/pub/2023-FASE.Software_Testing_5th_Comparative_Evaluation_Test-Comp_2023.pdf},
funding = {DFG-COOP},
}
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}
}
D. Beyer und S. Kanav, "CoVeriTeam: On-Demand Composition of Cooperative Verification Systems" in Proc. Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2022, Munich, Germany, April 2-7, 2022.
doi: 10.1007/978-3-030-99524-9_31
@inproceedings{TACAS22a,
author = {Dirk Beyer and Sudeep Kanav},
title = {{CoVeriTeam}: {O}n-Demand Composition of Cooperative Verification Systems},
booktitle = {Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2022, Munich, Germany, April 2-7},
editor = {D.~Fisman and G.~Rosu},
pages = {561-579},
year = {2022},
series = {LNCS~13243},
publisher = {Springer},
doi = {10.1007/978-3-030-99524-9_31},
sha256 = {e38311ae071351301b08d16849ee309a86efdc07fc45e18e466b4735ef21f241},
url = {https://www.sosy-lab.org/research/coveriteam/},
presentation = {https://www.sosy-lab.org/research/prs/2022-04-06_TACAS22_CoVeriTeam_Sudeep.pdf},
abstract = {},
keyword = {Software Model Checking,Cooperative Verification},
funding = {DFG-COOP},
}
D. Beyer, "Progress on Software Verification: SV-COMP 2022" in Proc. Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2022, Munich, Germany, April 2-7, 2022.
doi: 10.1007/978-3-030-99527-0_20
@inproceedings{TACAS22b,
author = {Dirk Beyer},
title = {Progress on Software Verification: {SV-COMP 2022}},
booktitle = {Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2022, Munich, Germany, April 2-7},
editor = {D.~Fisman and G.~Rosu},
pages = {375-402},
year = {2022},
series = {LNCS~13244},
publisher = {Springer},
doi = {10.1007/978-3-030-99527-0_20},
sha256 = {88d2b7552d79ad77c4e000f83a18f9d71038f7ddfca6c0f0700644405a115943},
url = {},
abstract = {},
keyword = {Competition on Software Verification (SV-COMP),Competition on Software Verification (SV-COMP Report),Software Model Checking},
_pdf = {https://www.sosy-lab.org/research/pub/2022-TACAS.Progress_on_Software_Verification_SV-COMP_2022.pdf},
funding = {DFG-COOP},
}
D. Beyer, S. Kanav, und C. Richter, "Construction of Verifier Combinations Based on Off-the-Shelf Verifiers" in Proc. Proceedings of the 25th International Conference on Fundamental Approaches to Software Engineering (FASE~2022, Munich, Germany, April 2-7), 2022.
doi: 10.1007/978-3-030-99429-7_3
@inproceedings{FASE22a,
author = {Dirk Beyer and Sudeep Kanav and Cedric Richter},
title = {Construction of Verifier Combinations Based on Off-the-Shelf Verifiers},
booktitle = {Proceedings of the 25th International Conference on Fundamental Approaches to Software Engineering (FASE~2022, Munich, Germany, April 2-7)},
editor = {E.~B.~Johnsen and M.~Wimmer},
pages = {49-70},
year = {2022},
series = {LNCS~13241},
publisher = {Springer},
isbn = {},
doi = {10.1007/978-3-030-99429-7_3},
sha256 = {fa50620b5b60e7c8761ea251b3ab30ef1e18320d49d76f417eac6dcd5b4a0bbc},
url = {https://www.sosy-lab.org/research/coveriteam-combinations/},
presentation = {https://www.sosy-lab.org/research/prs/2022-04-04_FASE22-CoVeriTeam-Combinations_Cedric.pdf},
abstract = {},
keyword = {Software Model Checking},
funding = {DFG-COOP},
}
D. Beyer, "Advances in Automatic Software Testing: Test-Comp 2022" in Proc. Proceedings of the 25th International Conference on Fundamental Approaches to Software Engineering (FASE~2022, Munich, Germany, April 2-7), 2022.
doi: 10.1007/978-3-030-99429-7_18
@inproceedings{FASE22b,
author = {Dirk Beyer},
title = {Advances in Automatic Software Testing: {Test-Comp 2022}},
booktitle = {Proceedings of the 25th International Conference on Fundamental Approaches to Software Engineering (FASE~2022, Munich, Germany, April 2-7)},
editor = {E.~B.~Johnsen and M.~Wimmer},
pages = {321-335},
year = {2022},
series = {LNCS~13241},
publisher = {Springer},
isbn = {},
doi = {10.1007/978-3-030-99429-7_18},
sha256 = {3f921c8f232a5c970f678889de8c402313049522a5dfa69ca68cd01d9dd9fce3},
url = {https://test-comp.sosy-lab.org/2022/},
abstract = {},
keyword = {Competition on Software Testing (Test-Comp),Competition on Software Testing (Test-Comp Report),Software Testing},
_pdf = {https://www.sosy-lab.org/research/pub/2022-FASE.Advances_in_Automatic_Software_Testing_Test-Comp_2022.pdf},
funding = {DFG-COOP},
}
D. Beyer und M. Jakobs, "Cooperative Verifier-Based Testing with CoVeriTest" International Journal on Software Tools for Technology Transfer (STTT), vol. 23, iss. 3.
doi: 10.1007/s10009-020-00587-8
@article{CoVeriTest-STTT,
author = {Dirk Beyer and Marie-Christine Jakobs},
title = {Cooperative Verifier-Based Testing with {CoVeriTest}},
journal = {International Journal on Software Tools for Technology Transfer (STTT)},
volume = {23},
number = {3},
pages = {313-333},
year = {2021},
doi = {10.1007/s10009-020-00587-8},
sha256 = {28a5bf6103296455728076e8c12902a53b3d377a296ea2ba18ac111c93330dbd},
url = {},
pdf = {},
presentation = {},
funding = {DFG-COOP},
issn = {1433-2787},
}
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}
}
D. Beyer, "Status Report on Software Testing: Test-Comp 2021" in Proc. Proceedings of the 24th International Conference on Fundamental Approaches to Software Engineering (FASE~2021, Luxembourg, Luxembourg, March 27 - April 1), 2021.
doi: 10.1007/978-3-030-71500-7_17
@inproceedings{FASE21,
author = {Dirk Beyer},
title = {Status Report on Software Testing: {Test-Comp 2021}},
booktitle = {Proceedings of the 24th International Conference on Fundamental Approaches to Software Engineering (FASE~2021, Luxembourg, Luxembourg, March 27 - April 1)},
editor = {E.~Guerra and M.~Stoelinga},
pages = {341-357},
year = {2021},
series = {LNCS~12649},
publisher = {Springer},
isbn = {978-3-030-71500-7},
doi = {10.1007/978-3-030-71500-7_17},
sha256 = {113b44c5be9f6d773ebd1a5cad91e8dc66f06d7af0b8c648c9dcea8d6bbc7e3d},
url = {https://test-comp.sosy-lab.org/2021/},
keyword = {Competition on Software Testing (Test-Comp),Competition on Software Testing (Test-Comp Report),Software Testing},
funding = {DFG-COOP},
}
D. Beyer, "First International Competition on Software Testing" International Journal on Software Tools for Technology Transfer (STTT), vol. 23, iss. 6.
doi: 10.1007/s10009-021-00613-3
@article{TestComp19-STTT,
author = {Dirk Beyer},
title = {First International Competition on Software Testing},
journal = {International Journal on Software Tools for Technology Transfer (STTT)},
volume = {23},
number = {6},
pages = {833-846},
year = {2021},
doi = {10.1007/s10009-021-00613-3},
sha256 = {cd82a853fbbf65de7f95a9e7de4f36118bb35fb516db87421a0aa38ccc863031},
url = {https://www.sosy-lab.org/research/pub/2021-STTT.First_International_Competition_on_Software_Testing.pdf},
pdf = {},
presentation = {},
abstract = {},
keyword = {Competition on Software Testing (Test-Comp),Competition on Software Testing (Test-Comp Report),Software Testing},
funding = {DFG-COOP},
issn = {1433-2787},
}
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 und M. Jakobs, "\sc FRed: Conditional Model Checking via Reducers and Folders" in Proc. Proceedings of the 18th International Conference on Software Engineering and Formal Methods (SEFM~2020, Virtual, Netherlands, September 14-18), 2020.
doi: 10.1007/978-3-030-58768-0_7
@inproceedings{SEFM20a,
author = {Dirk Beyer and Marie-Christine Jakobs},
title = {{{\sc FRed}}: {C}onditional Model Checking via Reducers and Folders},
booktitle = {Proceedings of the 18th International Conference on Software Engineering and Formal Methods (SEFM~2020, Virtual, Netherlands, September 14-18)},
editor = {F.~d.~Boer and A.~Cerone},
pages = {113--132},
year = {2020},
series = {LNCS~12310},
publisher = {Springer},
doi = {10.1007/978-3-030-58768-0_7},
sha256 = {0ce35cbde24d7a9de0513b89f23a81147bf4f8d5880effd57742c7f195e0eeec},
url = {https://www.sosy-lab.org/research/fred/},
abstract = {},
keyword = {CPAchecker,Software Model Checking},
funding = {DFG-COOP},
isbnnote = {},
}
D. Beyer, M. Jakobs, und T. Lemberger, "Difference Verification with Conditions" in Proc. Proceedings of the 18th International Conference on Software Engineering and Formal Methods (SEFM~2020, Virtual, Netherlands, September 14-18), 2020.
doi: 10.1007/978-3-030-58768-0_8
@inproceedings{SEFM20b,
author = {Dirk Beyer and Marie-Christine Jakobs and Thomas Lemberger},
title = {Difference Verification with Conditions},
booktitle = {Proceedings of the 18th International Conference on Software Engineering and Formal Methods (SEFM~2020, Virtual, Netherlands, September 14-18)},
editor = {F.~d.~Boer and A.~Cerone},
pages = {133--154},
year = {2020},
series = {LNCS~12310},
publisher = {Springer},
doi = {10.1007/978-3-030-58768-0_8},
sha256 = {8e5219da9a998b26f59013c809fbb1db6f92e3f08125fa1bfaacafcfafafef7f},
url = {https://www.sosy-lab.org/research/difference/},
presentation = {https://www.sosy-lab.org/research/prs/2020-09-17_SEFM20_DifferenceVerificationWithConditions_Thomas.pdf},
keyword = {CPAchecker,Software Model Checking},
funding = {DFG-COOP,DFG-CONVEY},
isbnnote = {},
video = {https://youtu.be/dG02602c9oo},
}
D. Beyer und T. Lemberger, "TestCov: Robust Test-Suite Execution and Coverage Measurement" in Proc. Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering (ASE 2019, San Diego, CA, USA, November 11-15), 2019.
doi: 10.1109/ASE.2019.00105
@inproceedings{ASE19,
author = {Dirk Beyer and Thomas Lemberger},
title = {{T}est{C}ov: Robust Test-Suite Execution and Coverage Measurement},
booktitle = {Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering (ASE 2019, San Diego, CA, USA, November 11-15)},
pages = {1074-1077},
year = {2019},
publisher = {IEEE},
doi = {10.1109/ASE.2019.00105},
sha256 = {},
pdf = {https://www.sosy-lab.org/research/pub/2019-ASE.TestCov_Robust_Test-Suite_Execution_and_Coverage_Measurement.pdf},
presentation = {https://www.sosy-lab.org/research/prs/2019-11-12_ASE19_TestCov_Thomas_Lemberger.pdf},
keyword = {Software Testing},
funding = {DFG-COOP},
isbnnote = {978-1-7281-2508-4},
}
D. Beyer und T. Lemberger, "Conditional Testing - Off-the-Shelf Combination of Test-Case Generators" in Proc. Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA~2019, Taipei, Taiwan, October 28-31), 2019.
doi: 10.1007/978-3-030-31784-3_11
@inproceedings{ATVA19,
author = {Dirk Beyer and Thomas Lemberger},
title = {Conditional Testing - Off-the-Shelf Combination of Test-Case Generators},
booktitle = {Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA~2019, Taipei, Taiwan, October 28-31)},
editor = {Yu{-}Fang Chen and Chih{-}Hong Cheng and Javier Esparza},
pages = {189-208},
year = {2019},
series = {LNCS~11781},
publisher = {Springer},
doi = {10.1007/978-3-030-31784-3_11},
sha256 = {},
url = {https://www.sosy-lab.org/research/conditional-testing/},
pdf = {https://www.sosy-lab.org/research/pub/2019-ATVA.Conditional_Testing_Off-the-Shelf_Combination_of_Test-Case_Generators.pdf},
presentation = {https://www.sosy-lab.org/research/prs/2019-10-29_ATVA19_Conditional_Testing_Thomas_Lemberger.pdf},
keyword = {Software Testing},
funding = {DFG-COOP},
}
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}
}
