Software and Computational Systems Lab

Publications by year

1. Daniel Bilic. Verification of Java Micro Services based on OpenAPI Specifications. Master's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking
   BibTeX Entry

   @misc{BilicOpenAPI, author = {Daniel Bilic}, title = {Verification of Java Micro Services based on OpenAPI Specifications}, year = {2024}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
2. Nils Sirrenberg. Certifying Software Violation Witnesses for Hardware Verification Tasks via Simulation-Based Validation. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Btor2, Witness-Based Validation PDF
   BibTeX Entry

   @misc{SirrenbergBtor2ViolationWitness, author = {Nils Sirrenberg}, title = {Certifying Software Violation Witnesses for Hardware Verification Tasks via Simulation-Based Validation}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Sirrenberg.Certifying_Software_Violation_Witnesses_for_Hardware_Verification_Tasks_via_Simulation-Based_Validation.restricted.pdf}, keyword = {Btor2, Witness-Based Validation}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
3. Jiacheng Chen. Automated Verification of the C Implementation of memcached with AFL++. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
   BibTeX Entry

   @misc{ChenMemcachedVerificationAFL, author = {Jiacheng Chen}, title = {Automated Verification of the C Implementation of memcached with AFL++}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Chen.Automated_Verification_of_the_C_Implementation_of_memcached_with_AFL++.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
4. Jinke Li. Automated Verification of the C Implementation of memcached with Goblint. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
   BibTeX Entry

   @misc{LiMemcachedVerificationGoblint, author = {Jinke Li}, title = {Automated Verification of the C Implementation of memcached with Goblint}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Li.Automated_Verification_of_the_C_Implementation_of_memcached_with_Goblint.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
5. Khac Ming Le. Automated Verification of the C Implementation of memcached with FuSeBMC. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
   BibTeX Entry

   @misc{LeMemcachedVerificationFuSeBMC, author = {Khac Ming Le}, title = {Automated Verification of the C Implementation of memcached with FuSeBMC}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Le.Automated_Verification_of_the_C_Implementation_of_memcached_with_FuSeBMC.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
6. Enno Muehlbauer. Automated Verification of the C Implementation of memcached with Ultimate Automizer. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
   BibTeX Entry

   @misc{MuehlbauerMemcachedVerificationUAutomizer, author = {Enno Muehlbauer}, title = {Automated Verification of the C Implementation of memcached with Ultimate Automizer}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Muehlbauer.Automated_Verification_of_the_C_Implementation_of_memcached_with_Ultimate_Automizer.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
7. Karim Triki. Automated Verification of the C Implementation of memcached with Taipan. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
   BibTeX Entry

   @misc{TrikiMemcachedVerificationTaipan, author = {Karim Triki}, title = {Automated Verification of the C Implementation of memcached with Taipan}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Triki.Automated_Verification_of_the_C_Implementation_of_memcached_with_Taipan.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
8. Ahmad Ghanem. Automated Verification of the C Implementation of memcached with ESBMC. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
   BibTeX Entry

   @misc{GhanemMemcachedVerificationESBMC, author = {Ahmad Ghanem}, title = {Automated Verification of the C Implementation of memcached with ESBMC}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Ghanem.Automated_Verification_of_the_C_Implementation_of_memcached_with_ESBMC.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
9. Yu-Chieh Lin. Automated Verification of the C Implementation of memcached with CPAchecker and k-Induction. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
   BibTeX Entry

   @misc{LinMemcachedVerificationCPAchecker, author = {Yu-Chieh Lin}, title = {Automated Verification of the C Implementation of memcached with CPAchecker and k-Induction}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Lin.Automated_Verification_of_the_C_Implementation_of_memcached_with_CPAchecker_and_K-Induction.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
10. Kai Müller. Automated Verification of the C Implementation of memcached with Klee. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
    BibTeX Entry

    @misc{MuellerMemcachedVerificationKlee, author = {Kai Müller}, title = {Automated Verification of the C Implementation of memcached with Klee}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Mueller.Automated_Verification_of_the_C_Implementation_of_memcached_with_Klee.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
11. Rania Qteishat. Automated Verification of the C Implementation of memcached with CBMC. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
    BibTeX Entry

    @misc{QteishatMemcachedVerificationCBMC, author = {Rania Qteishat}, title = {Automated Verification of the C Implementation of memcached with CBMC}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Qteishat.Automated_Verification_of_the_C_Implementation_of_memcached_with_CBMC.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
12. Dinghao Shi. Automated Verification of the C Implementation of memcached with AFL++. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
    BibTeX Entry

    @misc{ShiMemcachedVerificationAFL, author = {Dinghao Shi}, title = {Automated Verification of the C Implementation of memcached with AFL++}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Shi.Automated_Verification_of_the_C_Implementation_of_memcached_with_AFL++.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
13. Tong Wu. Automated Verification of the C Implementation of memcached with Goblint. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
    BibTeX Entry

    @misc{WuMemcachedVerificationGoblint, author = {Tong Wu}, title = {Automated Verification of the C Implementation of memcached with Goblint}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Wu.Automated_Verification_of_the_C_Implementation_of_memcached_with_Goblint.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
14. Marko Ristic. A Library for Unit Verification. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
    BibTeX Entry

    @misc{RisticUnitVerification, author = {Marko Ristic}, title = {A Library for Unit Verification}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Ristic.A_Library_for_Unit_Verification.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }

1. Benedikt Damböck. Verification of Java Programs with Exceptions with CPAchecker. Master's Thesis, LMU Munich, Software Systems Lab, 2023. Keyword(s): CPAchecker, Software Model Checking PDF Presentation
   BibTeX Entry

   @misc{DamboeckJavaExceptions, author = {Benedikt Damböck}, title = {Verification of Java Programs with Exceptions with CPAchecker}, year = {2023}, pdf = {https://www.sosy-lab.org/research/msc/2023.Damboeck.Verification_of_Java_Programs_with_Exceptions_with_CPAchecker.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2023-12-06_MA_Verification_of_Java_Programs_with_Exceptions_with_CPAchecker_Damboeck.pdf}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
2. Charlotte Gall. Updating the BenchExec Core Assignment for Modern CPU Architecture. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2023. Keyword(s): Benchmarking
   BibTeX Entry

   @misc{GallBenchexecCoreAssignment, author = {Charlotte Gall}, title = {Updating the BenchExec Core Assignment for Modern CPU Architecture}, year = {2023}, keyword = {Benchmarking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
3. Jens Linden. Scaling Formal Verification: Parallel Analysis of Functions in CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2023.
   BibTeX Entry

   @misc{LindenParallelAnalysis, author = {Jens Linden}, title = {Scaling Formal Verification: Parallel Analysis of Functions in CPAchecker}, year = {2023}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
4. Moritz Bierwirth. Designing and Assessing a Benchmark Set for Fault Localization Using Fault Injection. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2023. Keyword(s): Benchmarks PDF
   BibTeX Entry

   @misc{BierwirthFLBenchmarks, author = {Moritz Bierwirth}, title = {Designing and Assessing a Benchmark Set for Fault Localization Using Fault Injection}, year = {2023}, pdf = {https://www.sosy-lab.org/research/bsc/2023.Bierwirth.Designing_and_Assessing_a_Benchmark_Set_for_Fault_Localization_Using_Fault_Injection.pdf}, keyword = {Benchmarks}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
5. Salih Ates. Improving the Encoding of Arrays in Btor2-to-C Translation. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2023. Keyword(s): Btor2, Arrays PDF Presentation
   BibTeX Entry

   @misc{AtesBtor2CArray, author = {Salih Ates}, title = {Improving the Encoding of Arrays in Btor2-to-C Translation}, year = {2023}, pdf = {https://www.sosy-lab.org/research/bsc/2023.Ates.Improving_the_Encoding_of_Arrays_in_Btor2-to-C_Translation.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2023-08-30_BA_Improving_the_Encoding_of_Arrays_in_Btor2-to-C_Translation_Salih_Ates.pdf}, keyword = {Btor2, Arrays}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
6. Dusica Weisbarth. Ethics-based requirements analysis for a triage software: a case study. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2023.
   BibTeX Entry

   @misc{WeisbarthAnforderungsanalyse, author = {Dusica Weisbarth}, title = {Ethics-based requirements analysis for a triage software: a case study}, year = {2023}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }

1. Matthias Dangl. Witness-Based Validation of Verification Results with Applications to Software-Model Checking. PhD Thesis, LMU Munich, Software Systems Lab, 2022. doi:10.5282/edoc.31508 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF
   BibTeX Entry

   @misc{DanglWitnesses, author = {Matthias Dangl}, title = {Witness-Based Validation of Verification Results with Applications to Software-Model Checking}, year = {2022}, doi = {10.5282/edoc.31508}, url = {}, pdf = {https://edoc.ub.uni-muenchen.de/31508/3/Dangl_Matthias.pdf}, presentation = {}, keyword = {CPAchecker,Software Model Checking}, annote = {Now at ARS, Munich, Germany}, howpublished = {PhD Thesis, LMU Munich, Software Systems Lab}, urn = {urn:nbn:de:bvb:19-315089}, }
   Additional Infos

   Now at ARS, Munich, Germany
2. Thomas Lemberger. Towards Cooperative Software Verification with Test Generation and Formal Verification. PhD Thesis, LMU Munich, Software Systems Lab, 2022. doi:10.5282/edoc.32852 Keyword(s): CPAchecker, Software Model Checking, Cooperative Verification Publisher's Version PDF Presentation
   BibTeX Entry

   @misc{LembergerCoop, author = {Thomas Lemberger}, title = {Towards Cooperative Software Verification with Test Generation and Formal Verification}, year = {2022}, doi = {10.5282/edoc.32852}, url = {}, pdf = {https://edoc.ub.uni-muenchen.de/32852/1/Lemberger_Thomas.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2022-12-12_PhD_TowardsCooperativeSoftwareVerification_Thomas.pdf}, keyword = {CPAchecker,Software Model Checking,Cooperative Verification}, annote = {Nominated for the <a href="https://se2024.se.jku.at/ernst-denert-se-preis/">Ernst Denert SE-Preis 2024</a>}, howpublished = {PhD Thesis, LMU Munich, Software Systems Lab}, urn = {urn:nbn:de:bvb:19-328522}, }
   Additional Infos

   Nominated for the Ernst Denert SE-Preis 2024
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 : 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 \textsc{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 . 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 \textsc{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 . 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 \textsc{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}, }

1. 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}, }
2. Simon Antonischki. A CPA for String Analysis for Java Programs in . 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}, }
3. Penelope Powers. Mutation based Automatic Program Repair in . 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}, }
4. 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}, }
5. 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}, }
6. 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}, }
7. Sebastian Tschoepel. Implementation and Evaluation of a Simple Taint Analysis for . 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}, }
8. Dennis Simon. Shareable Benchmarking Reports with Enhanced Filters and Dynamic Statistics for . 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}, }
9. 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}, }
10. 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}, }
11. 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}, }
12. 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}, }
13. 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}, }
14. 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}, }

1. Moritz Beck. Solver-based Analysis of Memory Safety using Separation Logic. Master's Thesis, LMU Munich, Software Systems Lab, 2020. Keyword(s): CPAchecker, JavaSMT, Separation Logic, Software Model Checking PDF Presentation
   BibTeX Entry

   @misc{BeckSeparationLogic, author = {Moritz Beck}, title = {Solver-based Analysis of Memory Safety using Separation Logic}, year = {2020}, pdf = {https://www.sosy-lab.org/research/msc/2020.Beck.Solver-based_Analysis_of_Memory_Safety_using_Separation_Logic.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2020-09-16_MA_SolverBasedAnalysisOfMemorySafetyUsingSeparationLogic_Beck.pdf}, keyword = {CPAchecker,JavaSMT,Separation Logic,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
2. Martin Zehendner. Software Verification with Numerical Domains in . Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{ZehendnerNumericalDomains, author = {Martin Zehendner}, title = {Software Verification with Numerical Domains in \textsc{CPAchecker}}, year = {2020}, keyword = {CPAchecker, Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
3. Sven Umbricht. Converting Between ACSL Annotations and Witness Invariants. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Keyword(s): CPAchecker, Software Model Checking, ACSL PDF Presentation
   BibTeX Entry

   @misc{UmbrichtACSL, author = {Sven Umbricht}, title = {Converting Between ACSL Annotations and Witness Invariants}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Umbricht.Converting.Between.ACSL.Annotations.and.Witness.Invariants.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2021-02-10_BA_Converting.Between.ACSL.Annotations.and.Witness.Invariants_Umbricht.pdf}, keyword = {CPAchecker, Software Model Checking, ACSL}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
4. Benedikt Damböck. Implementierung und Evaluation von einfacher Schleifenabstraktion für das . Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Keyword(s): CPAchecker, Software Model Checking, Loop Acceleration
   BibTeX Entry

   @misc{DamboeckLoopAccel, author = {Benedikt Damböck}, title = {Implementierung und Evaluation von einfacher Schleifenabstraktion für das \textsc{CPAchecker}-Framework}, year = {2020}, keyword = {CPAchecker, Software Model Checking, Loop Acceleration}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
5. Sven Massard. Improve Analysis of Java Programs in . Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{MassardJavaPrograms, author = {Sven Massard}, title = {Improve Analysis of Java Programs in \textsc{CPAchecker}}, year = {2020}, keyword = {CPAchecker, Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
6. Frederic Schönberger. Converting Test Goals to Condition Automata. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Keyword(s): CPAchecker, Software Model Checking PDF Presentation
   BibTeX Entry

   @misc{SchoenbergerTestGoalsToConditions, author = {Frederic Sch{\"o}nberger}, title = {Converting Test Goals to Condition Automata}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Schoenberger.Converting_Test_Goals_to_Condition_Automata.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2021-01-13_BA_Converting_Test_Goals_to_Condition_Automata_Schoenberger.pdf}, keyword = {CPAchecker, Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
7. Jakob Selberg. Automatic Generation of Test Harnesses for Pointer-Based C Programs: Implementation of a Pointer-Tracking Analysis and Harness-Generation Engine in the Formal Verification Framework . Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{SelbergHarnessesForPointers, author = {Jakob Selberg}, title = {Automatic Generation of Test Harnesses for Pointer-Based C Programs: Implementation of a Pointer-Tracking Analysis and Harness-Generation Engine in the Formal Verification Framework \textsc{CPAchecker}}, year = {2020}, keyword = {CPAchecker, Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
8. Yannick Adams. Domain Types for Predicate Analysis in . Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{AdamsDomainTypesPredicate, author = {Yannick Adams}, title = {Domain Types for Predicate Analysis in \textsc{CPAchecker}}, year = {2020}, keyword = {CPAchecker, Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
9. Vladyslav Kolesnykov. SMT-Based Model Checking of Concurrent Programs. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Keyword(s): CPAchecker, Software Model Checking PDF
   BibTeX Entry

   @misc{KolesnykovConcurrencySMT, author = {Vladyslav Kolesnykov}, title = {{SMT}-Based Model Checking of Concurrent Programs}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Kolesnykov.SMT-Based_Model_Checking_of_Concurrent_Programs.pdf}, keyword = {CPAchecker, Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
10. Radu-Cristian Rusanu. Interval-Based Optimization for SMT Solvers. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Keyword(s): JavaSMT
    BibTeX Entry

    @misc{RusanuIntervalSMTSolver, author = {Radu-Cristian Rusanu}, title = {Interval-Based Optimization for SMT Solvers}, year = {2020}, keyword = {JavaSMT}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
11. Amena Abdulla. Reale Anforderungen für die Software-Analyse. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020.
    BibTeX Entry

    @misc{AbdullaSARD, author = {Amena Abdulla}, title = {Reale Anforderungen f{\"u}r die Software-Analyse}, year = {2020}, keyword = {}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
12. Simon Lund. Code Complexity Measures in Software Engineering: A Systematic Comparison and Evaluation on Software-Component Level. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. PDF
    BibTeX Entry

    @misc{LundComplexityMeasures, author = {Simon Lund}, title = {Code Complexity Measures in Software Engineering: A Systematic Comparison and Evaluation on Software-Component Level}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Lund.Complexity_Measures_in_Software_Engineering.pdf}, keyword = {}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
13. Angelos Kafounis. Fault Localization in Model Checking. Implementation and Evaluation of Fault-Localization Techniques with Distance Metrics. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Keyword(s): CPAchecker, Software Model Checking PDF Presentation
    BibTeX Entry

    @misc{KafounisFaultLocalizationWithDistanceMetrics, author = {Angelos Kafounis}, title = {Fault Localization in Model Checking. Implementation and Evaluation of Fault-Localization Techniques with Distance Metrics}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Kafounis.Fault_Localization_in_Model_Checking_Implementation_and_Evaluation_of_Fault-Localization_Techniques_with_Distance_Metrics.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2020-09-29_BA_FaultLocalizationWithDistanceMetrics_Kafounis.pdf}, keyword = {CPAchecker, Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
14. Schindar Ali. Test-Based Fault Localization in the Context of Formal Verification: Implementation and Evaluation of the Tarantula Algorithm in CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Keyword(s): CPAchecker, Software Model Checking PDF Presentation
    BibTeX Entry

    @misc{AliFaultLocalizationWithTarantula, author = {Schindar Ali}, title = {Test-Based Fault Localization in the Context of Formal Verification: Implementation and Evaluation of the Tarantula Algorithm in CPAchecker}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Ali.Test-Based_Fault_Localization_in_the_Context_of_Formal_Verification.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2020-09-02_BA_FaultLocalizationWithTestBasedDistanceMetrics_Ali.pdf}, keyword = {CPAchecker, Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
15. Petros Isaakidis. Energy Consumption Prediction of Verification Work. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Keyword(s): CPAchecker, Benchmarking, Energy Measurement
    BibTeX Entry

    @misc{IsaakidisEnergy, author = {Petros Isaakidis}, title = {Energy Consumption Prediction of Verification Work}, year = {2020}, keyword = {CPAchecker, Benchmarking, Energy Measurement}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
16. Matthias Kettl. Fault Localization for Formal Verification: An Implementation and Evaluation of Algorithms based on Error Invariants and UNSAT-cores. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Keyword(s): CPAchecker, Software Model Checking PDF Presentation
    BibTeX Entry

    @misc{KettlFaultLocalization, author = {Matthias Kettl}, title = {Fault Localization for Formal Verification: An Implementation and Evaluation of Algorithms based on Error Invariants and UNSAT-cores}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Kettl.Fault_Localization_for_Formal_Verification_An_Implementation_and_Evaluation_of_Algorithms_based_on_Error_Invariants_and_UNSAT-cores.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2020-07-22_BA_FaultLocalizationWithUnsatCores_Kettl.pdf}, keyword = {CPAchecker, Software Model Checking}, annote = {Won the LMU research award for excellent students (LMU Forschungspreis f{\"u}r exzellente Studierende) of LMU Munich}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
    Additional Infos

    Won the LMU research award for excellent students (LMU Forschungspreis für exzellente Studierende) of LMU Munich
17. Sonja Münchow. A Web Frontend For Visualization of Computation Steps and their Results in CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Keyword(s): CPAchecker PDF Presentation
    BibTeX Entry

    @misc{MuenchowVisualizeComputationSteps, author = {Sonja M\"unchow}, title = {A Web Frontend For Visualization of Computation Steps and their Results in CPAchecker}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Muenchow.A_Web_Frontend_for_Visualization_of_Computation_Steps_and_their_Results_in_CPAchecker.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2020-07-15_BA_WebFrontendForVisualizationOfComputationStepsInCpachecker_Muenchow.pdf}, keyword = {CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
18. Adrian Leimeister. A Language Server and IDE Plugin for . Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Keyword(s): CPAchecker PDF Presentation
    BibTeX Entry

    @misc{LeimeisterIdeLsp, author = {Adrian Leimeister}, title = {A Language Server and IDE Plugin for \textsc{CPAchecker}}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Leimeister.A_Language_Server_and_IDE_Plugin_for_CPAchecker.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2020-07-15_BA_IdePluginForCpachecker_Leimeister.pdf}, keyword = {CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
19. Michael Obermeier. Extending the Framework JavaSMT with the SMT Solver Yices2. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Keyword(s): JavaSMT PDF Presentation
    BibTeX Entry

    @misc{ObermeierYices2, author = {Michael Obermeier}, title = {Extending the Framework {{\sc JavaSMT}} with the {SMT} Solver {{\sc Yices2}}}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Obermeier.Extending_the_Framework_JavaSMT_with_the_SMT_Solver_Yices2.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2020-05-13_BA_IntegrationYices2InJavaSMT_Obermeier.pdf}, keyword = {JavaSMT}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
20. Alexander Ried. Design and Implementation of a Cluster-Based Approach for Software Verification. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Keyword(s): CPAchecker, BAM
    BibTeX Entry

    @misc{RiedClusterBAM, author = {Alexander Ried}, title = {Design and Implementation of a Cluster-Based Approach for Software Verification}, year = {2020}, keyword = {CPAchecker, BAM}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
21. Tillmann Gaida. SMT-based Checking and Synthesis of Formal Refinements. Master's Thesis, LMU Munich, Software Systems Lab, 2020.
    BibTeX Entry

    @misc{GaidaRefinement, author = {Tillmann Gaida}, title = {SMT-based Checking and Synthesis of Formal Refinements}, year = {2020}, field = {Computer Science}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
22. Lukas Rieger. Information Flow Testing of a PGP Server. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020.
    BibTeX Entry

    @misc{RiegerPGP, author = {Lukas Rieger}, title = {Information Flow Testing of a PGP Server}, year = {2020}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
23. Hyunsung Kim. Coverage-guided Fuzzing with Stochastic Optimization. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020.
    BibTeX Entry

    @misc{KimFuzzing, author = {Hyunsung Kim}, title = {Coverage-guided Fuzzing with Stochastic Optimization}, year = {2020}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }

1. Sabine Bauer. Decidability of Linear Tree Constraints for Resource Analysis of Object-Oriented Programs. PhD Thesis, LMU Munich, Software Systems Lab, 2019. doi:10.5282/edoc.24526 Publisher's Version PDF
   BibTeX Entry

   @misc{BauerDecidability, author = {Sabine Bauer}, title = {Decidability of Linear Tree Constraints for Resource Analysis of Object-Oriented Programs}, year = {2019}, doi = {10.5282/edoc.24526}, url = {}, pdf = {https://edoc.ub.uni-muenchen.de/24526/7/Bauer_Sabine.pdf}, presentation = {}, keyword = {}, annote = {}, howpublished = {PhD Thesis, LMU Munich, Software Systems Lab}, urn = {urn:nbn:de:bvb:19-245263}, }
2. Alexander Koos. Implementation and Evaluation of a Framework for Canonization and Caching of SMT Formulae. Master's Thesis, LMU Munich, Software Systems Lab, 2019. Keyword(s): JavaSMT, Software Model Checking
   BibTeX Entry

   @misc{KoosSMTCanonisationCaching, author = {Alexander Koos}, title = {Implementation and Evaluation of a Framework for Canonization and Caching of {SMT} Formulae}, year = {2019}, keyword = {JavaSMT,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
3. Stephan Holzner. Design und Implementierung einer parallelen BDD-Bibliothek. Master's Thesis, LMU Munich, Software Systems Lab, 2019. Keyword(s): BDD, Software Model Checking PDF
   BibTeX Entry

   @misc{HolznerParallelBDD, author = {Stephan Holzner}, title = {{Design und Implementierung einer parallelen BDD-Bibliothek}}, year = {2019}, pdf = {https://www.sosy-lab.org/research/msc/2019.Holzner.Design_und_Implementierung_einer_parallelen_BDD-Bibliothek.pdf}, keyword = {BDD,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
4. Michael Maier. SMT-Based Verification of ECMAScript Programs in CPAchecker. Master's Thesis, LMU Munich, Software Systems Lab, 2019. Keyword(s): CPAchecker, Software Model Checking PDF Presentation
   BibTeX Entry

   @misc{MichaelJavascript, author = {Michael Maier}, title = {{SMT}-Based Verification of {ECMAScript} Programs in {{\sc CPAchecker}}}, year = {2019}, pdf = {https://www.sosy-lab.org/research/msc/2019.Maier.SMT_Based_Verification_of_ECMAScript_Programs_in_CPAchecker.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2019-06-26_MA_SMTBasedVerificationOfECMAScriptProgramsInCPAchecker_Maier.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
5. Mirjam Trapp. Heuristics for Effective Predicate Refinement in CPAchecker. Master's Thesis, LMU Munich, Software Systems Lab, 2019. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{MirjamRefinement, author = {Mirjam Trapp}, title = {Heuristics for Effective Predicate Refinement in {{\sc CPAchecker}}}, year = {2019}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
6. Thomas Bunk. LTL Software Model Checking in CPAchecker. Master's Thesis, LMU Munich, Software Systems Lab, 2019. Keyword(s): CPAchecker, Software Model Checking PDF Presentation
   BibTeX Entry

   @misc{ThomasLTL, author = {Thomas Bunk}, title = {{LTL} Software Model Checking in {{\sc CPAchecker}}}, year = {2019}, pdf = {https://www.sosy-lab.org/research/msc/2019.Bunk.LTL_Software_Model_Checking_in_CPAchecker.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2019-03-27_MA_LtlSoftwareModelChecking_Bunk.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
7. Maximilian Hailer. Measuring and Optimizing Energy Consumption of Verification Work on Clusters. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019. Keyword(s): Benchmarking, Energy Measurement PDF Presentation
   BibTeX Entry

   @misc{HailerEnergy, author = {Maximilian Hailer}, title = {Measuring and Optimizing Energy Consumption of Verification Work on Clusters}, year = {2019}, pdf = {https://www.sosy-lab.org/research/bsc/2019.Hailer.Measuring_and_Optimizing_Energy_Consumption_of_Verification_Work_on_Clusters.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2019-10-30_BA_MeasuringAndOptimizingEnergyConsumptionOfVerificationWork_Hailer.pdf}, keyword = {Benchmarking, Energy Measurement}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
8. Daniel Baier. Integration des SMT-Solvers Boolector in das Framework JavaSMT und Evaluation mit CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019. Keyword(s): JavaSMT PDF Presentation
   BibTeX Entry

   @misc{BaierBoolector, author = {Daniel Baier}, title = {{Integration des SMT-Solvers Boolector in das Framework {{\sc JavaSMT}} und Evaluation mit {{\sc CPAchecker}}}}, year = {2019}, pdf = {https://www.sosy-lab.org/research/bsc/2019.Baier.Integration_des_SMT-Solvers_Boolector_in_das_Framework_JavaSMT_und_Evaluation_mit_CPAchecker.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2019-11-27_BA_IntegrationBoolectorInJavaSMT_Baier.pdf}, keyword = {JavaSMT}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
9. Laura Bschor. Modern Architecture and Improved UI for Tables of BenchExec. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019. Keyword(s): Benchmarking PDF Presentation
   BibTeX Entry

   @misc{BschorTables, author = {Laura Bschor}, title = {Modern Architecture and Improved {UI} for Tables of {{\sc BenchExec}}}, year = {2019}, pdf = {https://www.sosy-lab.org/research/bsc/2019.Bschor.Modern_Architecture_and_Improved_UI_for_Tables_of_BenchExec.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2019-11-06_BA_ModernArchitectureAndImprovedUIforTablesOfBenchExec_Bschor.pdf}, keyword = {Benchmarking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
10. Maximilian Wiesholler. Correctness Witness Validation using Predicate Analysis. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019. Keyword(s): CPAchecker, Software Model Checking, Witness-Based Validation PDF Presentation
    BibTeX Entry

    @misc{WieshollerWitnesses, author = {Maximilian Wiesholler}, title = {Correctness Witness Validation using Predicate Analysis}, year = {2019}, pdf = {https://www.sosy-lab.org/research/bsc/2019.Wiesholler.Correctness_Witness_Validation_using_Predicate_Analysis.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2019-06-05_BA_CorrectnessWitnessValidationUsingPredicateAnalysis_Wiesholler.pdf}, keyword = {CPAchecker, Software Model Checking, Witness-Based Validation}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
11. Krutav Shah. Counterexample-Guided Abstraction Refinement for Interval Domain. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019. Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry

    @misc{ShahIntervalRefinement, author = {Krutav Shah}, title = {Counterexample-Guided Abstraction Refinement for Interval Domain}, year = {2019}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
12. Raphael Hagl. Hybrid Testcase Generation with CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019. Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry

    @misc{HaglHybridExecution, author = {Raphael Hagl}, title = {Hybrid Testcase Generation with {{\sc CPAchecker}}}, year = {2019}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
13. Andrea Kreppel. Implementation and Evaluation of Backwards Analyses in the Software-Verification Framework CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019. Keyword(s): CPAchecker, Software Model Checking, Search Strategy PDF
    BibTeX Entry

    @misc{KreppelBackwardsAnalysis, author = {Andrea Kreppel}, title = {Implementation and Evaluation of Backwards Analyses in the Software-Verification Framework {{\sc CPAchecker}}}, year = {2019}, pdf = {https://www.sosy-lab.org/research/bsc/2019.Kreppel.Implementation_and_Evaluation_of_Backwards_Analyses_in_the_Software-Verification_Framework_CPAchecker.pdf}, keyword = {CPAchecker, Software Model Checking, Search Strategy}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
14. Gregor Alexandru. Specifying Loops with Contracts. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019. PDF
    BibTeX Entry

    @misc{AlexandruLoopContracts, author = {Gregor Alexandru}, title = {Specifying Loops with Contracts}, year = {2019}, pdf = {https://www.sosy-lab.org/research/bsc/2019.Alexandru.Specifying_Loops_With_Contracts.pdf}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
15. Leonhard Volk. Bipartite Matching Problems: Algorithms and Properties. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019.
    BibTeX Entry

    @misc{VolkBipartiteMatching, author = {Leonhard Volk}, title = {Bipartite Matching Problems: Algorithms and Properties}, year = {2019}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }

1. Gidon Ernst, Ichiro Hasuo, Zhenya Zhang, and Sean Sedwards. Time-staging Enhancement of Hybrid System Falsification. 2018. Presented at: Symbolic and Numerical Methods for Reachability Analysis (SNR). To appear in Proc. of SNR 2021. PDF
   BibTeX Entry

   @misc{ernst:snr2018, author = {Gidon Ernst and Ichiro Hasuo and Zhenya Zhang and Sean Sedwards}, title = {{Time-staging Enhancement of Hybrid System Falsification}}, year = {2018}, pdf = {https://www.sosy-lab.org/research/pub/2018-SNR.Time-staging_Enhancement_of_Hybrid_System_Falsification.pdf}, note = {Presented at: Symbolic and Numerical Methods for Reachability Analysis (SNR). To appear in Proc. of SNR 2021.}, }
2. Johannes Knaut. Symbolic Heap Abstraction with Automatic Refinement. Master's Thesis, LMU Munich, Software Systems Lab, 2018. Keyword(s): CPAchecker, Software Model Checking PDF
   BibTeX Entry

   @misc{JohannesSymbolicHeapRefinement, author = {Johannes Knaut}, title = {Symbolic Heap Abstraction with Automatic Refinement}, year = {2018}, pdf = {https://www.sosy-lab.org/research/msc/2018.Knaut.Symbolic_Heap_Abstraction_with_Automatic_Refinement.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
3. Martin Spiessl. Configurable Software Verification based on Slicing Abstractions. Master's Thesis, LMU Munich, Software Systems Lab, 2018. Keyword(s): CPAchecker, Software Model Checking PDF
   BibTeX Entry

   @misc{MartinSplitting, author = {Martin Spiessl}, title = {Configurable Software Verification based on Slicing Abstractions}, year = {2018}, pdf = {https://www.sosy-lab.org/research/msc/2018.Spiessl.Configurable_Software_Verification_based_on_Slicing_Abstractions.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
4. Thomas Lemberger. Abstraction Refinement for Model Checking: Program Slicing + CEGAR. Master's Thesis, LMU Munich, Software Systems Lab, 2018. Keyword(s): CPAchecker, Software Model Checking PDF
   BibTeX Entry

   @misc{ThomasSlicing, author = {Thomas Lemberger}, title = {Abstraction Refinement for Model Checking: Program Slicing + {CEGAR}}, year = {2018}, pdf = {https://www.sosy-lab.org/research/msc/2018.Lemberger.Abstraction_Refinement_for_Model_Checking_Program_Slicing_and_Cegar.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
5. Matthias Gerlach. Newton Refinement as Alternative to Craig Interpolation in CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018. Keyword(s): CPAchecker, Software Model Checking PDF Presentation
   BibTeX Entry

   @misc{GerlachNewtonRefinement, author = {Matthias Gerlach}, title = {Newton Refinement as Alternative to {Craig} Interpolation in {{\sc CPAchecker}}}, year = {2018}, pdf = {https://www.sosy-lab.org/research/bsc/2018.Gerlach.Newton_Refinement_as_Alternative_to_Craig_Interpolation_in_CPAchecker.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2019-01-09_BA_NewtonRefinementAsAlternativeToCraigInterpolationInCPAchecker_Gerlach.pdf}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
6. Flutura Estler. Heuristics-Based Selection of Verification Configurations. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{EstlerHeuristic, author = {Flutura Estler}, title = {Heuristics-Based Selection of Verification Configurations}, year = {2018}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
7. Balthasar Schuess. Flexible Online Job Scheduling in a Multi-User Environment. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018. Keyword(s): Cloud-Based Software Verification
   BibTeX Entry

   @misc{SchuessScheduling, author = {Balthasar Schuess}, title = {Flexible Online Job Scheduling in a Multi-User Environment}, year = {2018}, keyword = {Cloud-Based Software Verification}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
8. Dominik Friedrich. Konzeption, Umsetzung und Visualisierung von statistischen Daten in CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018. Keyword(s): CPAchecker
   BibTeX Entry

   @misc{FriedrichStatistics, author = {Dominik Friedrich}, title = {{Konzeption, Umsetzung und Visualisierung von statistischen Daten in CPAchecker}}, year = {2018}, keyword = {CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
9. Moritz Buhl. Application of Software Verification to OpenBSD Network Modules. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{BuhlOpenBSD, author = {Moritz Buhl}, title = {Application of Software Verification to {{\sc OpenBSD}} Network Modules}, year = {2018}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
10. Nicholas Reyes. Integrating a Witness Store into a Distributed Verification System. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018. Keyword(s): Witness-Based Validation, Cloud-Based Software Verification
    BibTeX Entry

    @misc{ReyesWitnessStore, author = {Nicholas Reyes}, title = {Integrating a Witness Store into a Distributed Verification System}, year = {2018}, keyword = {Witness-Based Validation,Cloud-Based Software Verification}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
11. Dominik Pastau. Implementation of a Generic Cloud-Based File-Storage Solution and its Integration into a Web-Based Distributed Verification System. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018. Keyword(s): Cloud-Based Software Verification
    BibTeX Entry

    @misc{PastauWitnessStore, author = {Dominik Pastau}, title = {Implementation of a Generic Cloud-Based File-Storage Solution and its Integration into a Web-Based Distributed Verification System}, year = {2018}, keyword = {Cloud-Based Software Verification}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
12. Karam Shabita. String Analysis for Java Programs in CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018. Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry

    @misc{SharamStrings, author = {Karam Shabita}, title = {String Analysis for {Java} Programs in {{\sc CPAchecker}}}, year = {2018}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }

1. Philipp Wendler. Towards Practical Predicate Analysis. PhD Thesis, University of Passau, Software Systems Lab, 2017. Keyword(s): Benchmarking, CPAchecker, Software Model Checking Publisher's Version PDF Presentation Supplement
   BibTeX Entry

   @misc{PhilippPredicateAnalysis, author = {Philipp Wendler}, title = {Towards Practical Predicate Analysis}, year = {2017}, url = {https://www.sosy-lab.org/research/phd/wendler/}, pdf = {https://www.sosy-lab.org/research/phd/2017.Wendler.Towards_Practical_Predicate_Analysis.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2017-11-20_RigorosumWendler_TowardsPracticalPredicateAnalysis.pdf}, keyword = {Benchmarking,CPAchecker,Software Model Checking}, annote = {Nominated for the <a href="https://gi.de/aktuelles/wettbewerbe/dissertationspreis/">Dissertation award 2017</a> of the German <a href="https://gi.de/">Gesellschaft f&uuml;r Informatik (GI)</a>}, howpublished = {PhD Thesis, University of Passau, Software Systems Lab}, urn = {urn:nbn:de:bvb:739-opus4-5098}, }
   Additional Infos

   Nominated for the Dissertation award 2017 of the German Gesellschaft für Informatik (GI)
2. Stefan Löwe. Effective Approaches to Abstraction Refinement for Automatic Software Verification. PhD Thesis, University of Passau, Software Systems Lab, 2017. Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
   BibTeX Entry

   @misc{StefanValueDomain, author = {Stefan L{\"{o}}we}, title = {Effective Approaches to Abstraction Refinement for Automatic Software Verification}, year = {2017}, url = {https://www.sosy-lab.org/research/phd/loewe/}, pdf = {https://www.sosy-lab.org/research/phd/2017.Loewe.Effective_Approaches_to_Abstraction_Refinement_for_Automatic_Software_Verification.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {PhD Thesis, University of Passau, Software Systems Lab}, urn = {urn:nbn:de:bvb:739-opus4-4815}, }
3. Evgeny Dunaev. Entwurf und Implementierung einer Abstraktionsschicht für Zuweisungs-basierte Analysen. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2017. Keyword(s): CPAchecker, Software Model Checking, Refactoring
   BibTeX Entry

   @misc{DunaevUnifyingAnalysis, author = {Evgeny Dunaev}, title = {{Entwurf und Implementierung einer Abstraktionsschicht f{\"u}r Zuweisungs-basierte Analysen}}, year = {2017}, keyword = {CPAchecker,Software Model Checking,Refactoring}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
4. Deyan Ivanov. Interactive Visualization of Verification Results from CPAchecker with D3. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2017. Keyword(s): CPAchecker, Software Model Checking PDF
   BibTeX Entry

   @misc{IvanovVisualization, author = {Deyan Ivanov}, title = {Interactive Visualization of Verification Results from {{\sc CPAchecker}} with {{\sc D3}}}, year = {2017}, pdf = {https://www.sosy-lab.org/research/bsc/2017.Ivanov.Interactive_Visualization_of_Verification_Results_from_CPAchecker_with_D3.pdf}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
5. Nils Steinger. Measuring, Visualizing, and Optimizing the Energy Consumption of Computer Clusters. Bachelor's Thesis, University of Passau, Software Systems Lab, 2017. Keyword(s): Benchmarking PDF Supplement
   BibTeX Entry

   @misc{SteingerMeasuring, author = {Nils Steinger}, title = {Measuring, Visualizing, and Optimizing the Energy Consumption of Computer Clusters}, year = {2017}, url = {https://www.sosy-lab.org/research/bsc/steinger}, pdf = {https://www.sosy-lab.org/research/bsc/2017.Steinger.Measuring,_Visualizing,_and_Optimizing_the_Energy_Consumption_of_Computer_Clusters.pdf}, keyword = {Benchmarking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }
6. Gernot Zoerneck. Implementing PDR in CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2017. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{ZoerneckPDR, author = {Gernot Zoerneck}, title = {Implementing {PDR} in {{\sc CPAchecker}}}, year = {2017}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }

1. Gidon Ernst. A Verified POSIX-Compliant Flash File System-Modular Verification Technology & Crash Tolerance. PhD Thesis, Augsburg University, 2016. PDF Supplement
   BibTeX Entry

   @misc{ernst:phd2016, author = {Gidon Ernst}, title = {A Verified {POSIX}-Compliant Flash File System---Modular Verification Technology \& Crash Tolerance}, year = {2016}, url = {https://isse.de/flashix}, pdf = {https://opus.bibliothek.uni-augsburg.de/opus4/files/3887/thesis_ernst.pdf}, howpublished = {PhD Thesis, Augsburg University}, }
2. Thomas Stieglmaier. Augmenting Predicate Analysis with Auxiliary Invariants. Master's Thesis, University of Passau, Software Systems Lab, 2016. Keyword(s): CPAchecker, Software Model Checking PDF Supplement
   BibTeX Entry

   @misc{ThomasInvariants, author = {Thomas Stieglmaier}, title = {Augmenting Predicate Analysis with Auxiliary Invariants}, year = {2016}, url = {https://www.sosy-lab.org/research/msc/stieglmaier}, pdf = {https://www.sosy-lab.org/research/msc/2016.Stieglmaier.Augmenting_Predicate_Analysis_with_Auxiliary_Invariants.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, }
3. Sebastian Ott. Implementing a Termination Analysis using Configurable Software Analysis. Master's Thesis, University of Passau, Software Systems Lab, 2016. Keyword(s): CPAchecker, Software Model Checking PDF
   BibTeX Entry

   @misc{SebastianTermination, author = {Sebastian Ott}, title = {Implementing a Termination Analysis using Configurable Software Analysis}, year = {2016}, pdf = {https://www.sosy-lab.org/research/msc/2016.Ott.Implementing_a_Termination_Analysis_using_Configurable_Program_Analysis.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, }
4. Stefan Weinzierl. Configurable Pointer-Alias Analysis in CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2016. Keyword(s): CPAchecker, Software Model Checking PDF
   BibTeX Entry

   @misc{WeinzierlPointerAliasing, author = {Stefan Weinzierl}, title = {Configurable Pointer-Alias Analysis in {{\sc CPAchecker}}}, year = {2016}, pdf = {https://www.sosy-lab.org/research/bsc/2016.Weinzierl.Configurable_Pointer-Alias_Analysis_for_CPAchecker.pdf}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }
5. Maximilian Syri. Verification of Concurrent Programs by CFA Sequentialization. Bachelor's Thesis, University of Passau, Software Systems Lab, 2016. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{SyriConcurrency, author = {Maximilian Syri}, title = {Verification of Concurrent Programs by {CFA} Sequentialization}, year = {2016}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }
6. Stephan Lukasczyk. Unbounded Heap Support for CPAchecker's Predicate Analysis Using SMT Arrays. Bachelor's Thesis, University of Passau, Software Systems Lab, 2016. Keyword(s): CPAchecker, Software Model Checking Supplement
   BibTeX Entry

   @misc{LukasczykPredicateHeap, author = {Stephan Lukasczyk}, title = {Unbounded Heap Support for {{\sc CPAchecker}}'s Predicate Analysis Using {SMT} Arrays}, year = {2016}, url = {https://research.lukasczyk.me/heaparray/}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }
7. Magdalena Murr. Towards Understandable CPAchecker Counterexamples. Bachelor's Thesis, University of Passau, Software Systems Lab, 2016. Keyword(s): CPAchecker, Software Model Checking PDF
   BibTeX Entry

   @misc{MurrCounterexampleReport, author = {Magdalena Murr}, title = {Towards Understandable {{\sc CPAchecker}} Counterexamples}, year = {2016}, pdf = {https://www.sosy-lab.org/research/bsc/2016.Murr.Towards_Understandable_CPAchecker_Counterexamples.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, subject = {Mobile and Embedded Systems}, }

1. BenchExec: Reliable Benchmarking and Resource Measurement. 2015. Keyword(s): Software Development Project Supplement
   BibTeX Entry

   @misc{BenchExec, title = {{{\sc BenchExec}}: Reliable Benchmarking and Resource Measurement}, year = {2015}, url = {https://github.com/dbeyer/BenchExec}, keyword = {Software Development Project}, role = {Contributor}, }
2. JavaSMT: A Unified Interface for SMT Solvers in Java. 2015. Keyword(s): Software Development Project, JavaSMT Supplement
   BibTeX Entry

   @misc{JavaSMT, title = {{{\sc JavaSMT}}: A Unified Interface for {SMT} Solvers in {Java}}, year = {2015}, url = {https://github.com/sosy-lab/java-smt}, keyword = {Software Development Project,JavaSMT}, role = {Contributor}, }
3. Karlheinz Friedberger. Block-Abstraction Memoization as an Approach to Verify Recursive Procedures. Master's Thesis, University of Passau, Software Systems Lab, 2015. Keyword(s): CPAchecker, Software Model Checking PDF
   BibTeX Entry

   @misc{KarlheinzBAMRecursion, author = {Karlheinz Friedberger}, title = {Block-Abstraction Memoization as an Approach to Verify Recursive Procedures}, year = {2015}, pdf = {https://www.sosy-lab.org/research/msc/2015.Friedberger.Block-Abstraction_Memoization_as_an_Approach_to_Verify_Recursive_Procedures.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, }
4. Thomas Lemberger. Efficient Symbolic Execution using CEGAR over Two Abstract Domains. Bachelor's Thesis, University of Passau, Software Systems Lab, 2015. Keyword(s): CPAchecker, Software Model Checking PDF
   BibTeX Entry

   @misc{ThomasSymbolicExecution, author = {Thomas Lemberger}, title = {Efficient Symbolic Execution using {CEGAR} over Two Abstract Domains}, year = {2015}, pdf = {https://www.sosy-lab.org/research/bsc/2015.Lemberger.Efficient_Symbolic_Execution_using_CEGAR_over_Two_Abstract_Domains.pdf}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }

1. Sebastian Ott. VerifierCloud: Implementierung eines Web-Service zur Software-Verifikation. Bachelor's Thesis, University of Passau, Software Systems Lab, 2014. Keyword(s): Cloud-Based Software Verification PDF
   BibTeX Entry

   @misc{SebastianVerifierCloud, author = {Sebastian Ott}, title = {{{\sc VerifierCloud}}: Implementierung eines Web-Service zur Software-Verifikation}, year = {2014}, pdf = {https://www.sosy-lab.org/research/bsc/2014.Ott.VerifierCloud__Implementierung_eines_Web-Service_zur_Software-Verifikation.pdf}, keyword = {Cloud-Based Software Verification}, field = {Computer Science}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }
2. Thomas Stieglmaier. Octagon-Based Software Verification with CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2014. Keyword(s): CPAchecker, Software Model Checking PDF
   BibTeX Entry

   @misc{ThomasOctagon, author = {Thomas Stieglmaier}, title = {Octagon-Based Software Verification with {{\sc CPAchecker}}}, year = {2014}, pdf = {https://www.sosy-lab.org/research/bsc/2014.Stieglmaier.Octagon-Based_Software_Verification_with_CPAchecker.pdf}, keyword = {CPAchecker,Software Model Checking}, field = {Internet Computing}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }
3. Georg Dresler. A Google-App-Engine Implementation for CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2014. Keyword(s): CPAchecker, Software Model Checking Supplement
   BibTeX Entry

   @misc{DreslerAppEngine, author = {Georg Dresler}, title = {A Google-App-Engine Implementation for {{\sc CPAchecker}}}, year = {2014}, url = {https://www.sosy-lab.org/download/appengine.pdf}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }

1. Matthias Dangl. Light-Weight Invariant Generation for Software Verification with CPAchecker. Master's Thesis, University of Passau, Software Systems Lab, 2013. Keyword(s): CPAchecker, Software Model Checking PDF
   BibTeX Entry

   @misc{MatthiasInvariantGeneration, author = {Matthias Dangl}, title = {Light-Weight Invariant Generation for Software Verification with {{\sc CPAchecker}}}, year = {2013}, pdf = {https://www.sosy-lab.org/research/msc/2015.Dangl.Light-Weight_Invariant_Generation_for_Software_Verification_with_CPAchecker.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, }
2. Matthias Dittrich. Bit-Precise Predicate Analysis with CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2013. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{DittrichBitprecisePredicate, author = {Matthias Dittrich}, title = {Bit-Precise Predicate Analysis with {{\sc CPAchecker}}}, year = {2013}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }

1. Christopher Jahn. Implementation of a CFA and ARG Visualization and Navigation Tool in Java. Master's Thesis, University of Passau, Software Systems Lab, 2012. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{JahnVisualization, author = {Christopher Jahn}, title = {Implementation of a {CFA} and {ARG} Visualization and Navigation Tool in {Java}}, year = {2012}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, }
2. Andreas Stahlbauer. Block-Encoding Strategies for Predicate Analysis: An Experimental Study. Master's Thesis, University of Passau, Software Systems Lab, 2012. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{StahlbauerStrategies, author = {Andreas Stahlbauer}, title = {Block-Encoding Strategies for Predicate Analysis: An Experimental Study}, year = {2012}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, permit = {Permission for making available online not granted (Dirk asked on 2020-07-17 and received denial on 2020-07-18)}, }
3. Peter Häring. A Comparative Study of Software Measures as Problem-Predictors. Master's Thesis, University of Passau, Software Systems Lab, 2012. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{HaeringMeasures, author = {Peter H{\"a}ring}, title = {A Comparative Study of Software Measures as Problem-Predictors}, year = {2012}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, permit = {}, }
4. Alexander Driemeyer. Software-Verifikation von Java-Programmen in CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2012. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{DriemeyerJava, author = {Alexander Driemeyer}, title = {Software-Verifikation von Java-Programmen in CPAchecker}, year = {2012}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }
5. Karlheinz Friedberger. Ein typbasierter Ansatz zur Kombination verschiedener Verifikationstechniken. Bachelor's Thesis, University of Passau, Software Systems Lab, 2012. Keyword(s): CPAchecker, Software Model Checking PDF
   BibTeX Entry

   @misc{KarlheinzDomainTypes, author = {Karlheinz Friedberger}, title = {{Ein typbasierter Ansatz zur Kombination verschiedener Verifikationstechniken}}, year = {2012}, pdf = {https://www.sosy-lab.org/research/bsc/2012.Friedberger.Ein_typbasierter_Ansatz_zur_Kombination_verschiedener_Verifikationstechniken.pdf}, keyword = {CPAchecker,Software Model Checking}, annote = {Won the yearly award of the chamber of industry and commerce of Lower Bavaria (IHK Niederbayern) for an excellent Bachelor's thesis}, field = {Computer Science}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }
   Additional Infos

   Won the yearly award of the chamber of industry and commerce of Lower Bavaria (IHK Niederbayern) for an excellent Bachelor's thesis

1. Mehmet Erkan Keremoglu. Towards Scalable Software Analyisis Using Combinations and Conditions with CPAchecker. PhD Thesis, Simon Fraser University, Software Systems Lab, 2011. Keyword(s): CPAchecker, Software Model Checking PDF Supplement
   BibTeX Entry

   @misc{ErkanCMC, author = {Mehmet Erkan Keremoglu}, title = {Towards Scalable Software Analyisis Using Combinations and Conditions with {{\sc CPAchecker}}}, year = {2011}, url = {https://summit.sfu.ca/item/12363}, pdf = {http://summit.sfu.ca/system/files/iritems1/12363/etd7320_MKeremoglu.pdf}, keyword = {CPAchecker,Software Model Checking}, annote = {Now at Microsoft, Redmond, USA}, howpublished = {PhD Thesis, Simon Fraser University, Software Systems Lab}, }
   Additional Infos

   Now at Microsoft, Redmond, USA
2. Andra-Maria Babau. Modeling and Verification of Airport Security Processes using BPMN and Protocol Interfaces: A Case Study. Master's Thesis, University of Passau, Software Systems Lab, 2011. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{BabauProtocolInterfaces, author = {Andra-Maria Babau}, title = {Modeling and Verification of Airport Security Processes using {BPMN} and Protocol Interfaces: A Case Study}, year = {2011}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, }

1. CheckDep: Tracking Software Dependencies. 2010. Keyword(s): Software Development Project, Structural Analysis and Comprehension Supplement
   BibTeX Entry

   @misc{CheckDep, title = {{{\sc CheckDep}}: Tracking Software Dependencies}, year = {2010}, url = {http://www.sosy-lab.org/~dbeyer/CheckDep/}, keyword = {Software Development Project,Structural Analysis and Comprehension}, role = {Principal designer, architect, and maintenance}, }
2. DepDigger: Detecting Complex Low-Level Dependencies. 2010. Keyword(s): Software Development Project, Structural Analysis and Comprehension Supplement
   BibTeX Entry

   @misc{DepDigger, title = {{{\sc DepDigger}}: Detecting Complex Low-Level Dependencies}, year = {2010}, url = {http://www.sosy-lab.org/~dbeyer/DepDigger/}, keyword = {Software Development Project,Structural Analysis and Comprehension}, role = {Principal designer, architect, and maintenance}, }
3. Grégory Théoduloz. Software Verification by Combining Program Analyses of Adjustable Precision. PhD Thesis, EPFL, MTC Lab, supervised by Prof. Thomas Henzinger, 2010. Keyword(s): BLAST, Software Model Checking PDF
   BibTeX Entry

   @misc{GregoryCPA, author = {Gr{\'e}gory Th{\'e}oduloz}, title = {Software Verification by Combining Program Analyses of Adjustable Precision}, year = {2010}, pdf = {https://doi.org/10.5075/epfl-thesis-4781}, keyword = {BLAST,Software Model Checking}, howpublished = {PhD Thesis, EPFL, MTC Lab, supervised by Prof. Thomas Henzinger}, }
4. Dmitry Balzer. Werkzeugunterstützung für Verstehen und Monitoring von Software-Abhängigkeiten. Master's Thesis, University of Passau, Software Systems Lab, 2010. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{BalzerDependencies, author = {Dmitry Balzer}, title = {{Werkzeugunterst{\"u}tzung f{\"u}r Verstehen und Monitoring von Software-Abh{\"a}ngigkeiten}}, year = {2010}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, }
5. Alexander von Rhein. Verification Tasks for Software Model Checking. Master's Thesis, University of Passau, Software Systems Lab, 2010. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{AlexQuery, author = {Alexander~von~Rhein}, title = {Verification Tasks for Software Model Checking}, year = {2010}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, }
6. Ashgan Fararooy. Performing Static Structure Analysis using Software Dependencies. Master's Thesis, Simon Fraser University, Software Systems Lab, 2010. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @misc{FararooyStructureAnalysis, author = {Ashgan Fararooy}, title = {Performing Static Structure Analysis using Software Dependencies}, year = {2010}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, Simon Fraser University, Software Systems Lab}, }
7. Philipp Wendler. Software Verification based on Adjustable Large-Block Encoding. Master's Thesis, University of Passau, Software Systems Lab, 2010. Keyword(s): CPAchecker, Software Model Checking PDF
   BibTeX Entry

   @misc{PhilippABE, author = {Philipp Wendler}, title = {Software Verification based on Adjustable Large-Block Encoding}, year = {2010}, pdf = {https://www.sosy-lab.org/research/msc/2010.Wendler.Software_Verification_based_on_Adjustable_Large-Block_Encoding.pdf}, keyword = {CPAchecker,Software Model Checking}, annote = {Won the NRW Young Scientist Award 2010 in Dynamic Intelligent Systems, received for the Faculty Award 2011 for best Master's thesis, and the yearly award of the Chamber of Industry and Commerce of Lower Bavaria (IHK Niederbayern) for an excellent Master's thesis}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, }
   Additional Infos

   Won the NRW Young Scientist Award 2010 in Dynamic Intelligent Systems, received for the Faculty Award 2011 for best Master's thesis, and the yearly award of the Chamber of Industry and Commerce of Lower Bavaria (IHK Niederbayern) for an excellent Master's thesis

1. Damien Zufferey. Master's Thesis, EPFL, MTC Lab, with Prof. Thomas Henzinger, 2009. Keyword(s): BLAST, Software Model Checking
   BibTeX Entry

   @misc{ZuffereyShape, author = {Damien Zufferey}, title = {}, year = {2009}, pdf = {}, keyword = {BLAST,Software Model Checking}, annote = {}, howpublished = {Master's Thesis, EPFL, MTC Lab, with Prof. Thomas Henzinger}, }

1. CSIsat: Interpolation for LA+EUF. 2008. Keyword(s): Software Development Project Supplement
   BibTeX Entry

   @misc{CSIsat, title = {{{\sc CSIsat}}: Interpolation for {LA+EUF}}, year = {2008}, url = {http://www.sosy-lab.org/~dbeyer/CSIsat/}, keyword = {Software Development Project}, role = {Contributor and designer}, }

1. CPAchecker: Configurable Software Verification. 2007. Keyword(s): Software Development Project, CPAchecker, Software Model Checking Supplement
   BibTeX Entry

   @misc{CPAchecker, title = {{{\sc CPAchecker}}: Configurable Software Verification}, year = {2007}, url = {http://www.sosy-lab.org/~dbeyer/CPAchecker/}, keyword = {Software Development Project,CPAchecker,Software Model Checking}, role = {Principal designer, architect, implementation, and maintenance}, }

1. Grégory Théoduloz. Integrating Shape Analysis into the Model Checker . Master's Thesis, EPFL, MTC Lab, with Prof. Thomas Henzinger, 2006. Keyword(s): BLAST, Software Model Checking
   BibTeX Entry

   @misc{TheodulozShape, author = {Gr{\'e}gory Th{\'e}oduloz}, title = {Integrating Shape Analysis into the Model Checker \textsc{Blast}}, year = {2006}, pdf = {}, keyword = {BLAST,Software Model Checking}, annote = {Won the EPFL Unicible Award 2006 and the ELCA Informatique Prize}, howpublished = {Master's Thesis, EPFL, MTC Lab, with Prof. Thomas Henzinger}, }
   Additional Infos

   Won the EPFL Unicible Award 2006 and the ELCA Informatique Prize

1. CCVisu: Visual Clustering and Software-Structure Assessment. 2005. Keyword(s): Software Development Project, Structural Analysis and Comprehension Supplement
   BibTeX Entry

   @misc{CCVisu, title = {{{\sc CCVisu}}: Visual Clustering and Software-Structure Assessment}, year = {2005}, url = {http://www.sosy-lab.org/~dbeyer/CCVisu/}, keyword = {Software Development Project,Structural Analysis and Comprehension}, role = {Principal designer and implementer}, }

1. Chic: Checking Interface Compatibility. 2004. Keyword(s): Software Development Project, Interfaces for Component-Based Design Supplement
   BibTeX Entry

   @misc{Chic, title = {{{\sc Chic}}: Checking Interface Compatibility}, year = {2004}, url = {http://www.sosy-lab.org/~dbeyer/Chic/}, keyword = {Software Development Project,Interfaces for Component-Based Design}, role = {Contributor, new formalism, and verification algorithm}, }

1. CrocoPat: Relational Programming (for Software-Structure Analysis). 2003. Keyword(s): Software Development Project, Structural Analysis and Comprehension Supplement
   BibTeX Entry

   @misc{CrocoPat, title = {{{\sc CrocoPat}}: Relational Programming (for Software-Structure Analysis)}, year = {2003}, url = {http://www.sosy-lab.org/~dbeyer/CrocoPat/}, keyword = {Software Development Project,Structural Analysis and Comprehension}, role = {Principal designer and implementer}, }

1. Blast: Model Checking of Software. 2002. Keyword(s): Software Development Project, Software Model Checking Supplement
   BibTeX Entry

   @misc{Blast, title = {{{\sc Blast}}: Model Checking of Software}, year = {2002}, url = {http://www.sosy-lab.org/~dbeyer/Blast/}, keyword = {Software Development Project,Software Model Checking}, role = {Contributor, conceptual extensions, implementation, and maintenance}, }

1. Andreas Noack. BDD-basierte Verifikation von Echtzeitsystemen. Master's Thesis, BTU Cottbus, with Prof. Claus Lewerentz, 2000. Keyword(s): Formal Verification of Real-Time Systems
   BibTeX Entry

   @misc{NoackBDD, author = {Andreas Noack}, title = {{BDD-basierte Verifikation von Echtzeitsystemen}}, year = {2000}, pdf = {}, keyword = {Formal Verification of Real-Time Systems}, annote = {Won the BTU University Award 2000 for best Master’s thesis}, howpublished = {Master's Thesis, BTU Cottbus, with Prof. Claus Lewerentz}, }
   Additional Infos

   Won the BTU University Award 2000 for best Master’s thesis

1. Rabbit: Verification of Real-Time Systems. 1998. Keyword(s): Software Development Project, Formal Verification of Real-Time Systems Supplement
   BibTeX Entry

   @misc{Rabbit, title = {{{\sc Rabbit}}: Verification of Real-Time Systems}, year = {1998}, url = {http://www.sosy-lab.org/~dbeyer/Rabbit/}, keyword = {Software Development Project,Formal Verification of Real-Time Systems}, role = {Principal designer and implementer}, }