Software and Computational Systems Lab

Publications of year 2021

1. Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen. TOOLympics II: Competitions on Formal Methods (Intro). International Journal on Software Tools for Technology Transfer (STTT), 23(6):879-881, 2021. doi:10.1007/s10009-021-00631-1 Publisher's Version PDF
   BibTeX Entry

   @article{Intro-TOOLympics2-STTT, author = {Dirk Beyer and Marieke Huisman and Fabrice Kordon and Bernhard Steffen}, title = {{TOOLympics II}: {Competitions} on Formal Methods (Intro)}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, volume = {23}, number = {6}, pages = {879-881}, year = {2021}, doi = {10.1007/s10009-021-00631-1}, sha256 = {efda377ea8f220771b05df7a9f9273bbcf6a692fa39f2a2304e7524408b8cdee}, url = {}, pdf = {}, presentation = {}, abstract = {}, keyword = {}, issn = {1433-2787}, }
2. Dirk Beyer. First International Competition on Software Testing. International Journal on Software Tools for Technology Transfer (STTT), 23(6):833-846, 2021. doi:10.1007/s10009-021-00613-3 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

   @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}, }
3. Dirk Beyer and Marieke Huisman. TOOLympics I: Competition on Software Testing (Intro). International Journal on Software Tools for Technology Transfer (STTT), 23(6):829-832, 2021. doi:10.1007/s10009-021-00611-5 Publisher's Version PDF
   BibTeX Entry

   @article{Intro-TOOLympics1-STTT, author = {Dirk Beyer and Marieke Huisman}, title = {{TOOLympics I}: {Competition} on Software Testing (Intro)}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, volume = {23}, number = {6}, pages = {829-832}, year = {2021}, doi = {10.1007/s10009-021-00611-5}, sha256 = {ec828ad46ee494c8fb08b462df617320f2ebce70c6bee9330c2f0eb65ef5d757}, url = {}, pdf = {}, presentation = {}, abstract = {}, keyword = {}, issn = {1433-2787}, }
4. Dirk Beyer and Marie-Christine Jakobs. Cooperative Verifier-Based Testing with CoVeriTest. International Journal on Software Tools for Technology Transfer (STTT), 23(3):313-333, 2021. doi:10.1007/s10009-020-00587-8 Keyword(s): CPAchecker, Software Model Checking, Software Testing Funding: DFG-COOP Publisher's Version PDF
   Abstract

   Testing is a widely applied technique to evaluate software quality, and coverage criteria are often used to assess the adequacy of a generated test suite. However, manually constructing an adequate test suite is typically too expensive, and numerous techniques for automatic test-suite generation were proposed. All of them come with different strengths. To build stronger test-generation tools, different techniques should be combined. In this paper, we study cooperative combinations of verification approaches for test generation, which exchange high-level information. We present CoVeriTest, a hybrid technique for test-suite generation. CoVeriTest iteratively applies different conditional model checkers and allows users to adjust the level of cooperation and to configure individual time limits for each conditional model checker. In our experiments, we systematically study different CoVeriTest cooperation setups, which either use combinations of explicit-state model checking and predicate abstraction, or bounded model checking and symbolic execution. A comparison with state-of-the-art test-generation tools reveals that CoVeriTest achieves higher coverage for many programs (about 15
   BibTeX Entry

   @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 = {}, abstract = {Testing is a widely applied technique to evaluate software quality, and coverage criteria are often used to assess the adequacy of a generated test suite. However, manually constructing an adequate test suite is typically too expensive, and numerous techniques for automatic test-suite generation were proposed. All of them come with different strengths. To build stronger test-generation tools, different techniques should be combined. In this paper, we study cooperative combinations of verification approaches for test generation, which exchange high-level information. We present CoVeriTest, a hybrid technique for test-suite generation. CoVeriTest iteratively applies different conditional model checkers and allows users to adjust the level of cooperation and to configure individual time limits for each conditional model checker. In our experiments, we systematically study different CoVeriTest cooperation setups, which either use combinations of explicit-state model checking and predicate abstraction, or bounded model checking and symbolic execution. A comparison with state-of-the-art test-generation tools reveals that CoVeriTest achieves higher coverage for many programs (about 15%).}, keyword = {CPAchecker,Software Model Checking,Software Testing}, funding = {DFG-COOP}, issn = {1433-2787}, }
5. Gidon Ernst, Sean Sedwards, Zhenya Zhang, and Ichiro Hasuo. Falsification of Hybrid Systems using Adaptive Probabilistic Search. Transact. on Modeling and Comp. Simulations (TOMACS), 31(3):1-22, 2021. ACM.
   BibTeX Entry

   @article{ernst:tomacs2021, author = {Gidon Ernst and Sean Sedwards and Zhenya Zhang and Ichiro Hasuo}, title = {Falsification of Hybrid Systems using Adaptive Probabilistic Search}, journal = {Transact. on Modeling and Comp. Simulations (TOMACS)}, volume = {31}, number = {3}, pages = {1--22}, year = {2021}, publisher = {ACM}, }
6. Martin Wirsing and Dieter Frey. Agile governance for innovating higher education teaching and learning. Rivista di Digital Politics(3/2021):543-558, 2021. Società editrice il Mulino. doi:10.53227/103804 Publisher's Version 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}, number = {3/2021}, pages = {543--558}, year = {2021}, publisher = {Società editrice il Mulino}, doi = {10.53227/103804}, pdf = {https://sosy-lab.org/research/pub/2022-Rivista.Agile_governance_for_innovating_higher_education_teaching_and_learning.pdf}, issn = {2785-0072}, urlpub = {https://www.rivisteweb.it/doi/10.53227/103804}, }
7. Lenz Belzner and Martin Wirsing. Synthesizing safe policies under probabilistic constraints with reinforcement learning and Bayesian model checking. Sci. Comput. Program., 206:102620, 2021. doi:10.1016/j.scico.2021.102620 Publisher's Version
   BibTeX Entry

   @article{DBLP:journals/scp/BelznerW21, author = {Lenz Belzner and Martin Wirsing}, title = {Synthesizing safe policies under probabilistic constraints with reinforcement learning and Bayesian model checking}, journal = {Sci. Comput. Program.}, volume = {206}, pages = {102620}, year = {2021}, doi = {10.1016/j.scico.2021.102620}, }
8. Simon Bliudze, Panagiotis Katsaros, Saddek Bensalem, and Martin Wirsing. On methods and tools for rigorous system design. Int. J. Softw. Tools Technol. Transf., 23(5):679-684, 2021. doi:10.1007/s10009-021-00632-0 Publisher's Version PDF
   BibTeX Entry

   @article{DBLP:journals/sttt/BliudzeKBW21, author = {Simon Bliudze and Panagiotis Katsaros and Saddek Bensalem and Martin Wirsing}, title = {On methods and tools for rigorous system design}, journal = {Int. J. Softw. Tools Technol. Transf.}, volume = {23}, number = {5}, pages = {679--684}, year = {2021}, doi = {10.1007/s10009-021-00632-0}, }

9. Dirk Beyer, Karlheinz Friedberger, and Stephan Holzner. PJBDD: A BDD Library for Java and Multi-Threading. In Proceedings of the 19th International Symposium on Automated Technology for Verification and Analysis (ATVA21 2021, Gold Coast (Online), Australia, October 18-22), 2021. Springer. doi:10.1007/978-3-030-88885-5_10 Keyword(s): PJBDD, BDD Funding: DFG-CONVEY Publisher's Version PDF
   Artifact(s)

   1. doi:10.5281/zenodo.5070156
   Abstract

   PJBDD is a flexible and modular Java library for binary decision diagrams (BDD), which are a well-known data structure for performing efficient operations on compressed sets and relations. BDDs have practical applications in composing and analyzing boolean functions, e.g., for computer-aided verification. Despite its importance, there are only a few BDD libraries available. PJBDD is based on a slim object-oriented design, supports multi-threaded execution of the BDD operations (internal) as well as thread-safe access to the operations from applications (external). It provides automatic reference counting and garbage collection. The modular design of the library allows us to provide a uniform API for binary decision diagrams, zero-suppressed decision diagrams, and also chained decision diagrams. This paper includes a compact evaluation of PJBDD, to demonstrate that concurrent operations on large BDDs scale well and parallelize nicely on multi-core CPUs.
   BibTeX Entry

   @inproceedings{ATVA21, author = {Dirk Beyer and Karlheinz Friedberger and Stephan Holzner}, title = {{PJBDD}: {A} {BDD} Library for {Java} and Multi-Threading}, booktitle = {Proceedings of the 19th International Symposium on Automated Technology for Verification and Analysis (ATVA21~2021, Gold Coast (Online), Australia, October 18-22)}, year = {2021}, publisher = {Springer}, doi = {10.1007/978-3-030-88885-5_10}, pdf = {https://www.sosy-lab.org/research/pub/2021-ATVA.PJBDD_A_BDD_Library_for_Java_and_Multi_Threading.pdf}, abstract = {PJBDD is a flexible and modular Java library for binary decision diagrams (BDD), which are a well-known data structure for performing efficient operations on compressed sets and relations. BDDs have practical applications in composing and analyzing boolean functions, e.g., for computer-aided verification. Despite its importance, there are only a few BDD libraries available. PJBDD is based on a slim object-oriented design, supports multi-threaded execution of the BDD operations (internal) as well as thread-safe access to the operations from applications (external). It provides automatic reference counting and garbage collection. The modular design of the library allows us to provide a uniform API for binary decision diagrams, zero-suppressed decision diagrams, and also chained decision diagrams. This paper includes a compact evaluation of PJBDD, to demonstrate that concurrent operations on large BDDs scale well and parallelize nicely on multi-core CPUs.}, keyword = {PJBDD,BDD}, artifact = {10.5281/zenodo.5070156}, funding = {DFG-CONVEY}, }
10. Daniel Baier, Dirk Beyer, and Karlheinz Friedberger. JavaSMT 3: Interacting with SMT Solvers in Java. In A. Silva and K. R. M. Leino, editors, Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV 2021, Los Angeles, California, USA, July 18-24), LNCS 12760, pages 1-13, 2021. Springer. doi:10.1007/978-3-030-81688-9_9 Keyword(s): JavaSMT Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{CAV21, author = {Daniel Baier and Dirk Beyer and Karlheinz Friedberger}, title = {JavaSMT 3: Interacting with SMT Solvers in Java}, booktitle = {Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV~2021, Los Angeles, California, USA, July 18-24)}, editor = {A.~Silva and K.~R.~M.~Leino}, pages = {1-13}, year = {2021}, series = {LNCS~12760}, publisher = {Springer}, doi = {10.1007/978-3-030-81688-9_9}, sha256 = {6c0ff13c5dd8596e19be4176eefaafe5853d60a082b78ebd3f5e64381fdcb100}, url = {https://github.com/sosy-lab/java-smt}, abstract = {}, keyword = {JavaSMT}, _pdf = {https://www.sosy-lab.org/research/pub/2021-CAV.JavaSMT_3_Interacting_with_SMT_Solvers_in_Java.pdf}, funding = {DFG-CONVEY}, }
11. Dirk Beyer. Software Verification: 10th Comparative Evaluation (SV-COMP 2021). In J. F. Groote and K. G. Larsen, editors, Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021, Luxembourg, Luxembourg, March 27 - April 1), part 2, LNCS 12652, pages 401-422, 2021. Springer. doi:10.1007/978-3-030-72013-1_24 Keyword(s): Competition on Software Verification (SV-COMP), Competition on Software Verification (SV-COMP Report), Software Model Checking Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{TACAS21, author = {Dirk Beyer}, title = {Software Verification: 10th Comparative Evaluation ({SV-COMP 2021})}, booktitle = {Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2021, Luxembourg, Luxembourg, March 27 - April 1), part 2}, editor = {J.~F.~Groote and K.~G.~Larsen}, pages = {401-422}, year = {2021}, series = {LNCS~12652}, publisher = {Springer}, doi = {10.1007/978-3-030-72013-1_24}, sha256 = {d78bb586715b0650702665510258d8e53a7bd16ae2a3cc4568b5986527b29051}, url = {https://sv-comp.sosy-lab.org/2021/}, abstract = {}, keyword = {Competition on Software Verification (SV-COMP),Competition on Software Verification (SV-COMP Report),Software Model Checking}, funding = {DFG-CONVEY}, }
12. Dirk Beyer. Status Report on Software Testing: Test-Comp 2021. In E. Guerra and M. Stoelinga, editors, Proceedings of the 24th International Conference on Fundamental Approaches to Software Engineering (FASE 2021, Luxembourg, Luxembourg, March 27 - April 1), LNCS 12649, pages 341-357, 2021. Springer. doi:10.1007/978-3-030-71500-7_17 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
    Abstract

    This report describes Test-Comp 2021, the 3rd edition of the Competition on Software Testing. The competition is a series of annual comparative evaluations of fully automatic software test generators for C programs. The competition has a strong focus on reproducibility of its results and its main goal is to provide an overview of the current state of the art in the area of automatic test-generation. The competition was based on 3 173 test-generation tasks for C programs. Each test-generation task consisted of a program and a test specification (error coverage, branch coverage). Test-Comp 2021 had 11 participating test generators from 6 countries.
    BibTeX Entry

    @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/}, abstract = {This report describes Test-Comp 2021, the 3rd edition of the Competition on Software Testing. The competition is a series of annual comparative evaluations of fully automatic software test generators for C programs. The competition has a strong focus on reproducibility of its results and its main goal is to provide an overview of the current state of the art in the area of automatic test-generation. The competition was based on 3 173 test-generation tasks for C programs. Each test-generation task consisted of a program and a test specification (error coverage, branch coverage). Test-Comp 2021 had 11 participating test generators from 6 countries.}, keyword = {Competition on Software Testing (Test-Comp),Competition on Software Testing (Test-Comp Report),Software Testing}, funding = {DFG-COOP}, }
13. Gidon Ernst, Johannes Blau, and Toby Murray. Deductive Verification via the Debug Adapter Protocol. In Proc. of Formal Integrated Development Environment (F-IDE), 2021.
    BibTeX Entry

    @inproceedings{ernst:fide2021, author = {Gidon Ernst and Johannes Blau and Toby Murray}, title = {Deductive Verification via the Debug Adapter Protocol}, booktitle = {Proc. of Formal Integrated Development Environment (F-IDE)}, year = {2021}, }
14. Grigory Fedyukovich and Gidon Ernst. Bridging Arrays and ADTs in Recursive Proofs. In Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, pages 24-42, 2021. Springer.
    BibTeX Entry

    @inproceedings{ernst:tacas2021, author = {Grigory Fedyukovich and Gidon Ernst}, title = {Bridging Arrays and {ADTs} in Recursive Proofs}, booktitle = {Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, volume = {12652}, pages = {24--42}, year = {2021}, series = {LNCS}, publisher = {Springer}, }
15. Gidon Ernst and others. ARCH-COMP 2021 category report: Falsification with Validation of Results. In Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH), EPiC, pages 133-152, 2021. EasyChair.
    BibTeX Entry

    @inproceedings{ernst:arch2021, author = {Gidon Ernst and others}, title = {{ARCH-COMP} 2021 category report: Falsification with Validation of Results}, booktitle = {Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH)}, volume = {80}, pages = {133--152}, year = {2021}, series = {EPiC}, publisher = {EasyChair}, }

16. Dirk Beyer, Lars Grunske, Thomas Lemberger, and Minxing Tang. Towards a Benchmark Set for Program Repair Based on Partial Fixes. Technical report 2107.08038, arXiv/CoRR, July 2021. doi:10.48550/arXiv.2107.08038 Publisher's Version PDF
    BibTeX Entry

    @techreport{TechReport21a, author = {Dirk Beyer and Lars Grunske and Thomas Lemberger and Minxing Tang}, title = {Towards a Benchmark Set for Program Repair Based on Partial Fixes}, number = {2107.08038}, year = {2021}, doi = {10.48550/arXiv.2107.08038}, keyword = {}, institution = {arXiv/CoRR}, month = {July}, }

17. Ludwig Glückstadt. Genetic Programming in Software Verification. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2021. Keyword(s): Software Model Checking, CPAchecker, Genetic Programming
    BibTeX Entry

    @misc{GlueckstadtGP, author = {Ludwig Glückstadt}, title = {Genetic Programming in Software Verification}, year = {2021}, keyword = {Software Model Checking, CPAchecker, Genetic Programming}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
18. Simon Antonischki. A CPA for String Analysis for Java Programs in CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2021. Keyword(s): Software Model Checking, CPAchecker
    BibTeX Entry

    @misc{AntonischkiStringCPA, author = {Simon Antonischki}, title = {A CPA for String Analysis for Java Programs in \textsc{CPAchecker}}, year = {2021}, keyword = {Software Model Checking, CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
19. Penelope Powers. Mutation based Automatic Program Repair in CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2021. Keyword(s): Automatic Program Repair, CPAchecker
    BibTeX Entry

    @misc{PowersAPR, author = {Penelope Powers}, title = {Mutation based Automatic Program Repair in \textsc{CPAchecker}}, year = {2021}, keyword = {Automatic Program Repair, CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
20. Korab Zogu. SV-COMP Benchmarks for Weak Memory Models. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2021. Keyword(s): Benchmarks, Weak Memory Models
    BibTeX Entry

    @misc{ZoguBenchmarksWeakMemoryModel, author = {Korab Zogu}, title = {SV-COMP Benchmarks for Weak Memory Models}, year = {2021}, keyword = {Benchmarks, Weak Memory Models}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
21. Yun Zhang. Verification Witnesses: from LLVM to C. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2021. Keyword(s): LLVM, Witness-Based Validation
    BibTeX Entry

    @misc{ZhangWitnessesLLVMToC, author = {Yun Zhang}, title = {Verification Witnesses: from LLVM to C}, year = {2021}, keyword = {LLVM, Witness-Based Validation}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
22. Simon Raths. Implementation and Evaluation of TBDDs in PJBDD. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2021. Keyword(s): BDD
    BibTeX Entry

    @misc{RathsTBDD, author = {Simon Raths}, title = {Implementation and Evaluation of TBDDs in PJBDD}, year = {2021}, keyword = {BDD}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
23. Sebastian Tschoepel. Implementation and Evaluation of a Simple Taint Analysis for CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2021. Keyword(s): CPAchecker, Software Model Checking, Taint
    BibTeX Entry

    @misc{TschoepelTaint, author = {Sebastian Tschoepel}, title = {Implementation and Evaluation of a Simple Taint Analysis for \textsc{CPAchecker}}, year = {2021}, keyword = {CPAchecker, Software Model Checking, Taint}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
24. Dennis Simon. Shareable Benchmarking Reports with Enhanced Filters and Dynamic Statistics for BenchExec. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2021. Keyword(s): Benchmarking PDF Presentation
    BibTeX Entry

    @misc{SimonBA, author = {Dennis Simon}, title = {Shareable Benchmarking Reports with Enhanced Filters and Dynamic Statistics for \textsc{BenchExec}}, year = {2021}, pdf = {https://www.sosy-lab.org/research/bsc/2021.Simon.Shareable_Benchmarking_Reports_with_Enhanced_Filters_and_Dynamic_Statistics_for_BenchExec.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2021-04-28_BA_ShareableBenchmarkingReportsWithEnhancedFiltersAndDynamicStatisticsForBenchExec_Simon.pdf}, keyword = {Benchmarking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
25. Matthias Kettl. A Collection of Real-World Benchmark Tasks for Repair of Partial Program Fixes. Research Internship, LMU Munich, Software Systems Lab, 2021.
    BibTeX Entry

    @misc{KettlPartialProgramFixesBenchmarkSet, author = {Matthias Kettl}, title = {A Collection of Real-World Benchmark Tasks for Repair of Partial Program Fixes}, year = {2021}, keyword = {}, howpublished = {Research Internship, LMU Munich, Software Systems Lab}, }
26. Lucas Hoffmann. Ulang-An experimental functional language and proof assistant. Master's Thesis, LMU Munich, Software Systems Lab, 2021.
    BibTeX Entry

    @misc{HoffmannUlang, author = {Lucas Hoffmann}, title = {Ulang---An experimental functional language and proof assistant}, year = {2021}, field = {Computer Science}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
27. Johannes Blau. Visual Verification Debugging in VS Code. Master's Thesis, LMU Munich, Software Systems Lab, 2021.
    BibTeX Entry

    @misc{BlauVisualDebugging, author = {Johannes Blau}, title = {Visual Verification Debugging in VS Code}, year = {2021}, field = {Computer Science}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
28. Christoph Girstenbrei. Combining Fuzzing and Symbolic Execution in CPAchecker. Master's Thesis, LMU Munich, Software Systems Lab, 2021.
    BibTeX Entry

    @misc{GirstenbreiFuzzing, author = {Christoph Girstenbrei}, title = {Combining Fuzzing and Symbolic Execution in CPAchecker}, year = {2021}, field = {Computer Science}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
29. Maximilian Doods. Python Frontend for a deductive verifier. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2021.
    BibTeX Entry

    @misc{DoodsPython, author = {Maximilian Doods}, title = {Python Frontend for a deductive verifier}, year = {2021}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
30. Marius Funk. Boogie front end for Cuvée. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2021.
    BibTeX Entry

    @misc{FunkBoogie, author = {Marius Funk}, title = {Boogie front end for Cuvée}, year = {2021}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }