Software and Computational Systems Lab

Publications of year 2022

1. Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann, Thomas Lemberger, and Michael Tautschnig. Verification Witnesses. ACM Trans. Softw. Eng. Methodol., 31(4):57:1-57:69, 2022. doi:10.1145/3477579 Publisher's Version PDF Supplement
   BibTeX Entry

   @article{Witnesses-TOSEM, author = {Dirk Beyer and Matthias Dangl and Daniel Dietsch and Matthias Heizmann and Thomas Lemberger and Michael Tautschnig}, title = {Verification Witnesses}, journal = {ACM Trans. Softw. Eng. Methodol.}, volume = {31}, number = {4}, pages = {57:1-57:69}, year = {2022}, doi = {10.1145/3477579}, url = {https://www.sosy-lab.org/research/verification-witnesses-tosem/}, _pdf = {https://www.sosy-lab.org/research/pub/2022-TOSEM.Verification_Witnesses.pdf}, _sha256 = {48acf3f35251df635e829b29fe8f16fd50498f8f99a082b8b9e0aa094a97a432}, }
2. Martin Wirsing and Dieter Frey. Agile governance for innovating higher education teaching and learning. Rivista di Digital Politics, 2022. To appear. PDF
   BibTeX Entry

   @article{WirsingF21, author = {Martin Wirsing and Dieter Frey}, title = {Agile governance for innovating higher education teaching and learning}, journal = {Rivista di Digital Politics}, year = {2022}, pdf = {https://sosy-lab.org/research/pub/2022-Rivista.Agile_governance_for_innovating_higher_education_teaching_and_learning.pdf}, doinone = {Unpublished: Last checked: 2022-03-07}, note = {To appear.}, }

1. Dirk Beyer and Andreas Podelski. Software Model Checking: 20 Years and Beyond. In Principles of Systems Design, LNCS 13660, pages 554-582, 2022. Springer. doi:10.1007/978-3-031-22337-2_27 Keyword(s): Software Model Checking Publisher's Version PDF
   BibTeX Entry

   @inproceedings{Henzinger22, author = {Dirk Beyer and Andreas Podelski}, title = {Software Model Checking: 20 Years and Beyond}, booktitle = {Principles of Systems Design}, pages = {554-582}, year = {2022}, series = {LNCS~13660}, publisher = {Springer}, doi = {10.1007/978-3-031-22337-2_27}, sha256 = {87a441617d1194266dff5fd5bd143370e9b318e72848b2d6e3c49f152a136799}, url = {}, abstract = {}, keyword = {Software Model Checking}, _pdf = {}, editors = {J-F.~Raskin and K.~Chatterjee and L.~Doyen and R.~Majumdar}, funding = {}, }
2. Dirk Beyer and Jan Strejček. Case Study on Verification-Witness Validators: Where We Are and Where We Go. In Proceedings of the 29th International Symposium on Static Analysis, (SAS 2022, Auckland, New Zealand, December 5-7, 2022), LNCS 13790, pages 160-174, 2022. Springer. doi:10.1007/978-3-031-22308-2_8 Keyword(s): Software Model Checking Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SAS22, author = {Dirk Beyer and Jan Strejček}, title = {Case Study on Verification-Witness Validators: Where We Are and Where We Go}, booktitle = {Proceedings of the 29th International Symposium on Static Analysis, (SAS~2022, Auckland, New Zealand, December 5-7, 2022)}, pages = {160-174}, year = {2022}, series = {LNCS~13790}, publisher = {Springer}, doi = {10.1007/978-3-031-22308-2_8}, sha256 = {8003de86c73be27da528c44f440a49cd03a877649c9cb61a328a37507bc963da}, url = {}, abstract = {}, keyword = {Software Model Checking}, _pdf = {}, editors = {Gagandeep Singh and Caterina Urban}, funding = {}, }
3. Dirk Beyer, Martin Spiessl, and Sven Umbricht. Cooperation between Automatic and Interactive Software Verifiers. In Bernd-Holger Schlingloff and Ming Chai, editors, Proceedings of the 20th International Conference on Software Engineering and Formal Methods, (SEFM 2022, Berlin, Germany, September 26-30, LNCS 13550, pages 111–128, 2022. Springer. doi:10.1007/978-3-031-17108-6_7 Keyword(s): Software Model Checking Funding: DFG-CONVEY Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SEFM22b, author = {Dirk Beyer and Martin Spiessl and Sven Umbricht}, title = {Cooperation between Automatic and Interactive Software Verifiers}, booktitle = {Proceedings of the 20th International Conference on Software Engineering and Formal Methods, (SEFM~2022, Berlin, Germany, September 26-30}, editor = {Bernd-Holger Schlingloff and Ming Chai}, pages = {111–128}, year = {2022}, series = {LNCS~13550}, publisher = {Springer}, doi = {10.1007/978-3-031-17108-6_7}, sha256 = {a310ff0ac97f37ee817c6f05a4cc9a635cbacd09ad301b483095f133040e8e48}, url = {}, abstract = {}, keyword = {Software Model Checking}, _pdf = {https://www.sosy-lab.org/research/pub/2022-SEFM.Cooperation_between_Automatic_and_Interactive_Software_Verifiers.pdf}, funding = {DFG-CONVEY}, }
4. Dirk Beyer, Marian Lingsch Rosenfeld, and Martin Spiessl. A Unifying Approach for Control-Flow-Based Loop Abstraction. In Bernd-Holger Schlingloff and Ming Chai, editors, Proceedings of the 20th International Conference on Software Engineering and Formal Methods, (SEFM 2022, Berlin, Germany, September 26-30, LNCS 13550, pages 3-19, 2022. Springer. doi:10.1007/978-3-031-17108-6_1 Keyword(s): Software Model Checking Funding: DFG-CONVEY Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SEFM22a, author = {Dirk Beyer and Marian Lingsch Rosenfeld and Martin Spiessl}, title = {A Unifying Approach for Control-Flow-Based Loop Abstraction}, booktitle = {Proceedings of the 20th International Conference on Software Engineering and Formal Methods, (SEFM~2022, Berlin, Germany, September 26-30}, editor = {Bernd-Holger Schlingloff and Ming Chai}, pages = {3-19}, year = {2022}, series = {LNCS~13550}, publisher = {Springer}, doi = {10.1007/978-3-031-17108-6_1}, sha256 = {047a8a9062e143741623320cf80ec963ce5f7200a5a75d263fa6615c12f2199e}, url = {}, abstract = {}, keyword = {Software Model Checking}, _pdf = {https://www.sosy-lab.org/research/pub/2022-SEFM.A_Unifying_Approach_for_Control-Flow-Based_Loop_Abstraction.pdf}, funding = {DFG-CONVEY}, }
5. Dirk Beyer, Jan Haltermann, Thomas Lemberger, and Heike Wehrheim. Decomposing Software Verification into Off-the-Shelf Components: An Application to CEGAR. In Proceedings of the 44th International Conference on Software Engineering (ICSE 2022, Pittsburgh, PA, USA, May 8-20 (Virtual), May 22-27 (In-Person)), pages 536-548, 2022. ACM. doi:10.1145/3510003.3510064 Keyword(s): CPAchecker, Software Model Checking, Interfaces for Component-Based Design Funding: DFG-COOP Publisher's Version PDF Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.5301636
   Abstract

   Techniques for software verification are typically realized as cohesive units of software with tightly coupled components. This makes it difficult to re-use components, and the potential for workload distribution is limited. Innovations in software verification might find their way into practice faster if provided in smaller, more specialized components. In this paper, we propose to strictly decompose software verification: the verification task is split into independent subtasks, implemented by only loosely coupled components communicating via clearly defined interfaces. We apply this decomposition concept to one of the most frequently employed techniques in software verification: counterexample-guided abstraction refinement (CEGAR). CEGAR is a technique to iteratively compute an abstract model of the system. We develop a decomposition of CEGAR into independent components with clearly defined interfaces that are based on existing, standardized exchange formats. Its realization component-based CEGAR (C-CEGAR) concerns the three core tasks of CEGAR: abstract-model exploration, feasibility check, and precision refinement. We experimentally show that - despite the necessity of exchanging complex data via interfaces - the efficiency thereby only reduces by a small constant factor while the precision in solving verification tasks even increases. We furthermore illustrate the advantages of C-CEGAR by experimenting with different implementations of components, thereby further increasing the overall effectiveness and testing that substitution of components works well.
   BibTeX Entry

   @inproceedings{ICSE22, 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 = {Proceedings of the 44th International Conference on Software Engineering (ICSE~2022, Pittsburgh, PA, USA, May 8-20 (Virtual), May 22-27 (In-Person))}, pages = {536-548}, year = {2022}, publisher = {ACM}, doi = {10.1145/3510003.3510064}, url = {https://www.sosy-lab.org/research/component-based-cegar/}, abstract = {Techniques for software verification are typically realized as cohesive units of software with tightly coupled components. This makes it difficult to re-use components, and the potential for workload distribution is limited. Innovations in software verification might find their way into practice faster if provided in smaller, more specialized components. In this paper, we propose to strictly decompose software verification: the verification task is split into independent subtasks, implemented by only loosely coupled components communicating via clearly defined interfaces. We apply this decomposition concept to one of the most frequently employed techniques in software verification: counterexample-guided abstraction refinement (CEGAR). CEGAR is a technique to iteratively compute an abstract model of the system. We develop a decomposition of CEGAR into independent components with clearly defined interfaces that are based on existing, standardized exchange formats. Its realization component-based CEGAR (C-CEGAR) concerns the three core tasks of CEGAR: abstract-model exploration, feasibility check, and precision refinement. We experimentally show that --- despite the necessity of exchanging complex data via interfaces --- the efficiency thereby only reduces by a small constant factor while the precision in solving verification tasks even increases. We furthermore illustrate the advantages of C-CEGAR by experimenting with different implementations of components, thereby further increasing the overall effectiveness and testing that substitution of components works well.}, keyword = {CPAchecker,Software Model Checking,Interfaces for Component-Based Design}, _pdf = {https://www.sosy-lab.org/research/pub/2022-ICSE.Decomposing_Software_Verification_into_Off-the-Shelf-Components.pdf}, _sha256 = {be1c5d744475af00f5a0cddd51d92353296d1d8e5ba60f5439ba5b98217e0e03}, artifact = {10.5281/zenodo.5301636}, funding = {DFG-COOP}, }
6. Dirk Beyer and Martin Spiessl. The Static Analyzer Frama-C in SV-COMP (Competition Contribution). In Dana Fisman and Grigore Rosu, editors, Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022, Munich, Germany, April 2-7, LNCS 13244, pages 429-434, 2022. Springer. doi:10.1007/978-3-030-99527-0_26 Keyword(s): Competition on Software Verification (SV-COMP), Software Model Checking Funding: DFG-CONVEY Publisher's Version PDF
   BibTeX Entry

   @inproceedings{TACAS22c, author = {Dirk Beyer and Martin Spiessl}, title = {The Static Analyzer {Frama-C} in {SV-COMP} (Competition Contribution)}, 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 = {Dana Fisman and Grigore Rosu}, pages = {429--434}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_26}, sha256 = {77ed425c2b30a4f9424ed46c9cb5a846f5c21677ececdbf098e30f37aca67a3d}, url = {}, abstract = {}, keyword = {Competition on Software Verification (SV-COMP),Software Model Checking}, _pdf = {https://www.sosy-lab.org/research/pub/2022-TACAS.The_Static_Analyzer_Frama-C_in_SV-COMP_Competition_Contribution.pdf}, funding = {DFG-CONVEY}, }
7. Dirk Beyer. Progress on Software Verification: SV-COMP 2022. In D. Fisman and G. Rosu, editors, Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022, Munich, Germany, April 2-7, LNCS 13244, pages 375-402, 2022. Springer. doi:10.1007/978-3-030-99527-0_20 Keyword(s): Competition on Software Verification (SV-COMP), Competition on Software Verification (SV-COMP Report), Software Model Checking Funding: DFG-COOP Publisher's Version PDF
   BibTeX Entry

   @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}, }
8. Dirk Beyer and Sudeep Kanav. CoVeriTeam: On-Demand Composition of Cooperative Verification Systems. In D. Fisman and G. Rosu, editors, Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022, Munich, Germany, April 2-7, LNCS 13243, pages 561-579, 2022. Springer. doi:10.1007/978-3-030-99524-9_31 Keyword(s): Software Model Checking Funding: DFG-COOP Publisher's Version PDF Presentation Supplement
   BibTeX Entry

   @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}, funding = {DFG-COOP}, }
9. Dirk Beyer. Advances in Automatic Software Testing: Test-Comp 2022. In E. B. Johnsen and M. Wimmer, editors, Proceedings of the 25th International Conference on Fundamental Approaches to Software Engineering (FASE 2022, Munich, Germany, April 2-7), LNCS 13241, pages 321-335, 2022. Springer. doi:10.1007/978-3-030-99429-7_18 Keyword(s): Competition on Software Testing (Test-Comp), Competition on Software Testing (Test-Comp Report), Software Testing Funding: DFG-COOP Publisher's Version PDF Supplement
   BibTeX Entry

   @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}, }
10. Dirk Beyer, Sudeep Kanav, and Cedric Richter. Construction of Verifier Combinations Based on Off-the-Shelf Verifiers. In E. B. Johnsen and M. Wimmer, editors, Proceedings of the 25th International Conference on Fundamental Approaches to Software Engineering (FASE 2022, Munich, Germany, April 2-7), LNCS 13241, pages 49-70, 2022. Springer. doi:10.1007/978-3-030-99429-7_3 Keyword(s): Software Model Checking Funding: DFG-COOP Publisher's Version PDF Presentation Supplement
    BibTeX Entry

    @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}, }
11. Dongge Liu, Van-Thuan Pham, Gidon Ernst, Toby Murray, and Benjamin Rubinstein. State selection algorithms and their impact on the performance of stateful network protocol fuzzing. In Proc. of Software Analysis, Evolution and Reengineering (SANER), 2022. IEEE. To appear.
    BibTeX Entry

    @inproceedings{ernst:saner2022, author = {Dongge Liu and Van-Thuan Pham and Gidon Ernst and Toby Murray and Benjamin Rubinstein}, title = {State selection algorithms and their impact on the performance of stateful network protocol fuzzing}, booktitle = {Proc. of Software Analysis, Evolution and Reengineering (SANER)}, year = {2022}, publisher = {IEEE}, note = {To appear.}, }
12. Gidon Ernst. Loop Verification with Invariants and Summaries. In Proc. of Verification, Model-Checking, and Abstract Interpretation (VMCAI), LNCS, 2022. Springer.
    BibTeX Entry

    @inproceedings{ernst:vmcai2022, author = {Gidon Ernst}, title = {Loop Verification with Invariants and Summaries}, booktitle = {Proc. of Verification, Model-Checking, and Abstract Interpretation (VMCAI)}, volume = {13182}, year = {2022}, series = {LNCS}, publisher = {Springer}, }
13. Matthias Kettl and Thomas Lemberger. The Static Analyzer Infer in SV-COMP (Competition Contribution). In Dana Fisman and Grigore Rosu, editors, Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022, Munich, Germany, April 2-7), Part 2, LNCS 13244, pages 451-456, 2022. Springer. doi:10.1007/978-3-030-99527-0_30 Keyword(s): Competition on Software Verification (SV-COMP) Publisher's Version PDF Presentation
    Abstract

    We present Infer-SV, a wrapper that adapts Infer for SV-COMP. Infer is a static-analysis tool for C and other languages, developed by Facebook and used by multiple large companies. It is strongly aimed at industry and the internal use at Facebook. Despite its popularity, there are no reported numbers on its precision and efficiency. With Infer-SV, we take a first step towards an objective comparison of Infer with other SV-COMP participants from academia and industry.
    BibTeX Entry

    @inproceedings{INFER-SVCOMP22, author = {Matthias Kettl and Thomas Lemberger}, title = {The Static Analyzer Infer in {SV-COMP} (Competition Contribution)}, 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), Part 2}, editor = {Dana Fisman and Grigore Rosu}, pages = {451--456}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_30}, pdf = {https://www.sosy-lab.org/research/pub/2022-SVCOMP.The_Static_Analyzer_Infer_in_SV-COMP.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2022-04-07_TACAS_Infer.pdf}, abstract = {We present Infer-SV, a wrapper that adapts Infer for SV-COMP. Infer is a static-analysis tool for C and other languages, developed by Facebook and used by multiple large companies. It is strongly aimed at industry and the internal use at Facebook. Despite its popularity, there are no reported numbers on its precision and efficiency. With Infer-SV, we take a first step towards an objective comparison of Infer with other SV-COMP participants from academia and industry.}, keyword = {Competition on Software Verification (SV-COMP)}, }

1. Dirk Beyer, Nian-Ze Lee, and Philipp Wendler. Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification. Technical report 2208.05046, arXiv/CoRR, August 2022. doi:10.48550/arXiv.2208.05046 Keyword(s): Software Model Checking, CPAchecker Publisher's Version PDF Presentation Supplement
   Abstract

   Interpolation-based model checking (McMillan, 2003) is a formal-verification algorithm, which was originally devised to verify safety properties of finite-state transition systems. The algorithm is state-of-the-art in hardware model checking. It derives interpolants from unsatisfiable BMC queries, and collects them to construct an overapproximation of the set of reachable states. Unlike other formal-verification algorithms, such as k-induction or PDR, which have been extended to handle infinite-state systems and investigated for program analysis, McMillan's interpolation-based model checking algorithm from 2003 has not been used to verify programs so far. This paper closes this significant, 19 years old gap in knowledge by adopting the algorithm to software verification. We implemented it in the verification framework CPAchecker, and evaluated the implementation against other state-of-the-art software-verification techniques over the largest publicly available benchmark suite of C safety-verification tasks. The evaluation demonstrates that interpolation-based model checking is competitive among other algorithms in terms of both the number of solved verification tasks and the run-time efficiency. Our results might have important implications for software verification, because researchers and developers now have a richer set of approaches to choose from.
   BibTeX Entry

   @techreport{TechReport22a, author = {Dirk Beyer and Nian-Ze Lee and Philipp Wendler}, title = {Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification}, number = {2208.05046}, year = {2022}, doi = {10.48550/arXiv.2208.05046}, url = {https://www.sosy-lab.org/research/cpa-imc/}, presentation = {https://www.sosy-lab.org/research/prs/2022-08-11_iPRA22_Interpolation_and_SAT-Based_Model_Checking_Revisited.pdf}, abstract = {Interpolation-based model checking (McMillan, 2003) is a formal-verification algorithm, which was originally devised to verify safety properties of finite-state transition systems. The algorithm is state-of-the-art in hardware model checking. It derives interpolants from unsatisfiable BMC queries, and collects them to construct an overapproximation of the set of reachable states. Unlike other formal-verification algorithms, such as k-induction or PDR, which have been extended to handle infinite-state systems and investigated for program analysis, McMillan's interpolation-based model checking algorithm from 2003 has not been used to verify programs so far. This paper closes this significant, 19 years old gap in knowledge by adopting the algorithm to software verification. We implemented it in the verification framework CPAchecker, and evaluated the implementation against other state-of-the-art software-verification techniques over the largest publicly available benchmark suite of C safety-verification tasks. The evaluation demonstrates that interpolation-based model checking is competitive among other algorithms in terms of both the number of solved verification tasks and the run-time efficiency. Our results might have important implications for software verification, because researchers and developers now have a richer set of approaches to choose from.}, keyword = {Software Model Checking, CPAchecker}, _pdf = {https://www.sosy-lab.org/research/cpa-imc/Interpolation_and_SAT-Based_Model_Checking_Revisited.pdf}, institution = {arXiv/CoRR}, month = {August}, }

1. Matthias Dangl. Witness-Based Validation of Verification Results with Applications to Software-Model Checking. PhD Thesis, LMU Munich, Software Systems Lab, 2022. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{DanglWitnesses, author = {Matthias Dangl}, title = {Witness-Based Validation of Verification Results with Applications to Software-Model Checking}, year = {2022}, url = {}, pdf = {}, presentation = {}, keyword = {CPAchecker,Software Model Checking}, annote = {}, doinone = {}, howpublished = {PhD Thesis, LMU Munich, Software Systems Lab}, urn = {}, }
2. Thomas Lemberger. Towards Cooperative Software Verification with Test Generation and Formal Verification. PhD Thesis, LMU Munich, Software Systems Lab, 2022. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{LembergerCoop, author = {Thomas Lemberger}, title = {Towards Cooperative Software Verification with Test Generation and Formal Verification}, year = {2022}, url = {}, pdf = {}, presentation = {}, keyword = {CPAchecker,Software Model Checking}, annote = {}, doinone = {}, howpublished = {PhD Thesis, LMU Munich, Software Systems Lab}, urn = {}, }
3. Karlheinz Friedberger. Efficient Software Model Checking with Block-Abstraction Memoization. PhD Thesis, LMU Munich, Software Systems Lab, 2022. doi:10.5282/edoc.29976 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF
   BibTeX Entry

   @misc{FriedbergerBAM, author = {Karlheinz Friedberger}, title = {Efficient Software Model Checking with Block-Abstraction Memoization}, year = {2022}, doi = {10.5282/edoc.29976}, url = {}, pdf = {https://edoc.ub.uni-muenchen.de/29976/1/Friedberger_Karlheinz.pdf}, presentation = {}, keyword = {CPAchecker,Software Model Checking}, annote = {Now at MSG Systems, Munich, Germany}, howpublished = {PhD Thesis, LMU Munich, Software Systems Lab}, urn = {urn:nbn:de:bvb:19-296471}, }
   Additional Infos

   Now at MSG Systems, Munich, Germany
4. Daniel Baier. Implementation of Value Analysis over Symbolic Memory Graphs in CPAchecker. Master's Thesis, LMU Munich, Software Systems Lab, 2022. Keyword(s): CPAchecker, Software Model Checking, Symbolic Memory Graphs PDF Presentation
   BibTeX Entry

   @misc{BaierSymbolicMemoryGraphs, author = {Daniel Baier}, title = {Implementation of Value Analysis over Symbolic Memory Graphs in CPAchecker}, year = {2022}, pdf = {https://www.sosy-lab.org/research/msc/2022.Baier.Implementation_of_Value_Analysis_over_Symbolic_Memory_Graphs_in_CPAchecker.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2022-09-28_MA_Implementation_of_Value_Analysis_over_Symbolic_Memory_Graphs_in_CPAchecker_Baier.pdf}, keyword = {CPAchecker,Software Model Checking,Symbolic Memory Graphs}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
5. Martin Pletl. A New Spin on Verification with Symbolic Execution: Symbolic Execution as Formula-Based Predicate Analysis in CPAchecker. Master's Thesis, LMU Munich, Software Systems Lab, 2022. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{PletlSymbolicExecution, author = {Martin Pletl}, title = {A New Spin on Verification with Symbolic Execution: Symbolic Execution as Formula-Based Predicate Analysis in CPAchecker}, year = {2022}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
6. Maximilian Hailer. New Approaches and Visualization for Verification Coverage. Master's Thesis, LMU Munich, Software Systems Lab, 2022. Keyword(s): CPAchecker, Software Model Checking PDF Presentation
   BibTeX Entry

   @misc{HailerVerificationCoverage, author = {Maximilian Hailer}, title = {New Approaches and Visualization for Verification Coverage}, year = {2022}, pdf = {https://www.sosy-lab.org/research/msc/2022.Hailer.New_Approaches_and_Visualization_for_Verification_Coverage.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2022-06-16_MA_New_Approaches_and_Visualization_for_Verification_Coverage_Hailer.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
7. Matthias Kettl. Adjustable Block Analysis: Actor-Based Creation of Block Summaries for Scaling Formal Verification. Master's Thesis, LMU Munich, Software Systems Lab, 2022. Keyword(s): CPAchecker, Software Model Checking PDF Presentation
   BibTeX Entry

   @misc{Kettl, author = {Matthias Kettl}, title = {Adjustable Block Analysis: Actor-Based Creation of Block Summaries for Scaling Formal Verification}, year = {2022}, pdf = {https://www.sosy-lab.org/research/msc/2022.Kettl.Adjustable_Block_Analysis.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2022-02-24_MA_Adjustable_Block_Analysis.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
8. Philipp Waldinger. Concurrent Software Verification through Block-based Task Partitioning and Continuous Summary Refinement. Master's Thesis, LMU Munich, Software Systems Lab, 2022. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{WaldingerTaskPartitioning, author = {Philipp Waldinger}, title = {Concurrent Software Verification through Block-based Task Partitioning and Continuous Summary Refinement}, year = {2022}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
9. Klara Cimbalnik. Program Transformation in CPAchecker. Design and Implementation of a Source-Respecting Translation from Control-Flow Automata to C Code. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2022. Keyword(s): CPAchecker
   BibTeX Entry

   @misc{CimbalnikCfaExport, author = {Klara Cimbalnik}, title = {Program Transformation in CPAchecker. Design and Implementation of a Source-Respecting Translation from Control-Flow Automata to C Code}, year = {2022}, keyword = {CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
10. Tobias Kleinert. Developing a Verifier Based on Parallel Portfolio with CoVeriTeam. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2022. Keyword(s): Benchmarking PDF Presentation
    BibTeX Entry

    @misc{KleinertParPortfolioCoVeriTeam, author = {Tobias Kleinert}, title = {Developing a Verifier Based on Parallel Portfolio with CoVeriTeam}, year = {2022}, pdf = {https://www.sosy-lab.org/research/bsc/2022.Kleinert.Parallel_Portfolio_CoVeriTeam.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2022-03-16_BA_Parallel_Portfolio_CoVeriTeam.pdf}, keyword = {Benchmarking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
11. Robin Gloster. Cgroups v2 Support for BenchExec. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2022. Keyword(s): Benchmarking PDF Presentation
    BibTeX Entry

    @misc{GlosterCgroupsV2, author = {Robin Gloster}, title = {Cgroups v2 Support for BenchExec}, year = {2022}, pdf = {https://www.sosy-lab.org/research/bsc/2022.Gloster.Cgroups_v2_Support_for_BenchExec.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2022-03-09_BA_Cgroups_v2_Support_for_BenchExec_Gloster.pdf}, keyword = {Benchmarking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }