Publications by year
2024
-
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}, } -
Creating an Exchangeable Intermediate Program Representation for the Formal Software Verifier CPAchecker.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2024.
Keyword(s):
CPAchecker
BibTeX Entry
@misc{LindenmeierCfaJsonExport, author = {Felix Lindenmeier}, title = {Creating an Exchangeable Intermediate Program Representation for the Formal Software Verifier CPAchecker}, year = {2024}, keyword = {CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, } -
Streamlining Software Verification: A Maven Plugin for Formal Verification of Java Code.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2024.
Keyword(s):
Software Model Checking
PDF
BibTeX Entry
@misc{MartinJbmcMavenPlugin, author = {Yannick Martin}, title = {Streamlining Software Verification: A Maven Plugin for Formal Verification of Java Code}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Martin.Streamlining_Software_Verification_A_Maven_Plugin_for_Formal_Verification_of_Java_Code.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, } -
From Compilation to Verification: Extending Gradle with JBMC for Enhanced Code Safety.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2024.
Keyword(s):
Software Model Checking
BibTeX Entry
@misc{DubchakJbmcGradlePlugin, author = {Ella Dubchak}, title = {From Compilation to Verification: Extending Gradle with JBMC for Enhanced Code Safety}, year = {2024}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, } -
Evaluation of JVM Garbage Collectors for CPAchecker.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2024.
Keyword(s):
CPAchecker,
Benchmarking
PDF
Presentation
BibTeX Entry
@misc{MagetEvaluationJVMGarbageCollectorsCPAchecker, author = {Tobias Maget}, title = {Evaluation of JVM Garbage Collectors for CPAchecker}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Maget.Evaluation_of_JVM_Garbage_Collectors_for_CPAchecker.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2024-10-23-BA_Evaluation_of_JVM_Garbage_Collectors_for_CPAchecker_Maget.pdf}, keyword = {CPAchecker, Benchmarking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, } -
Witness Modifications for Program Transformations: A Case Study on Side-Effect Removal.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2024.
Keyword(s):
Witnesses
PDF
BibTeX Entry
@misc{OvezovaWitnessModificationsSideEffectsCaseStudy, author = {Anna Ovezova}, title = {Witness Modifications for Program Transformations: A Case Study on Side-Effect Removal}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Ovezova.Witness_Modifications_for_Program_Transformations_A_Case_study_on_Side-Effect_Removal.pdf}, keyword = {Witnesses}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, } -
Verification of Micro Services based on Pact API Contracts.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2024.
Keyword(s):
Software Model Checking
PDF
BibTeX Entry
@misc{MattisMicroserviceVerification, author = {Robin Mattis}, title = {Verification of Micro Services based on Pact API Contracts}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Mattis.Verification_of_Micro_Services_based_on_Pact_API_Contracts.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
Auswahl des Testalgorithmus mittels boolescher Merkmale.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2024.
BibTeX Entry
@misc{TestAlgorithmSelection, author = {Khrystyna Reichel}, title = {Auswahl des Testalgorithmus mittels boolescher Merkmale}, year = {2024}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, } -
Auswahl der Zeitlimits für CoVeriTest mittels boolescher Merkmale.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2024.
BibTeX Entry
@misc{TestTimeSelection, author = {Iurii Irkha}, title = {Auswahl der Zeitlimits für CoVeriTest mittels boolescher Merkmale}, year = {2024}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
2023
-
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}, } -
Extending the Framework JavaSMT with the SMT Solver Bitwuzla and Evaluation using CPAchecker.
at LMU Munich, Bachelor's Thesis, LMU Munich, Software Systems Lab,
2023.
Keyword(s):
JavaSMT,
SMT,
Bitwuzla,
CPAchecker
PDF
BibTeX Entry
@misc{LindnerDefense, author = {Heinrich Dennis Simon Lindner}, title = {Extending the Framework JavaSMT with the SMT Solver Bitwuzla and Evaluation using CPAchecker}, year = {2023}, pdf = {2023.Lindner.Extending_the_Framework_JavaSMT_with_the_SMT_Solver_Bitwuzla_and_Evaluation_using_CPAchecker.pdf}, keyword = {JavaSMT, SMT, Bitwuzla, CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, venue = {LMU Munich}, } -
Extending the JavaSMT Framework with the Apron Library for Numerical Abstract Domain with subsequent Usability Assessment.
at LMU Munich, Bachelor's Thesis, LMU Munich, Software Systems Lab,
2023.
Keyword(s):
Apron,
SMT,
Abstract Interpretation,
JavaSMT
PDF
BibTeX Entry
@misc{RosBA, author = {Winnie Lilith Sofia Ros}, title = {Extending the JavaSMT Framework with the Apron Library for Numerical Abstract Domain with subsequent Usability Assessment}, year = {2023}, pdf = {2023.Ros.Extending_the_JavaSMT_Framework_with_the_Apron_Library_for_Numerical_Abstract_Domain_with_subsequent_Usability_Assessment.pdf}, keyword = {Apron, SMT, Abstract Interpretation, JavaSMT}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, venue = {LMU Munich}, } -
Adding the SMT solver OpenSMT2 to the JavaSMT Framework and Evaluation using CPAchecker.
at LMU Munich, Bachelor's Thesis, LMU Munich, Software Systems Lab,
2023.
Keyword(s):
SMT,
JavaSMT,
OpenSMT2,
CPAchecker
PDF
BibTeX Entry
@misc{RafflerBA, author = {Daniel Raffler}, title = {Adding the SMT solver OpenSMT2 to the JavaSMT Framework and Evaluation using CPAchecker}, year = {2023}, pdf = {2023.Raffler.Adding_the_SMT_solver_OpenSMT2_to_the_JavaSMT_Framework_and_Evaluation_using_CPAchecker.pdf}, keyword = {SMT, JavaSMT, OpenSMT2, CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, venue = {LMU Munich}, } -
Implementing a Solver-Independent SMT-LIB2 Parser-Interpreter and Code-Generator for JavaSMT with Subsequent Evaluation.
at LMU Munich, Bachelor's Thesis, LMU Munich, Software Systems Lab,
2023.
Keyword(s):
JavaSMT,
SMT-LIB2,
SMT,
CPAchecker
PDF
BibTeX Entry
@misc{KingBA, author = {Janelle King}, title = {Implementing a Solver-Independent SMT-LIB2 Parser-Interpreter and Code-Generator for JavaSMT with Subsequent Evaluation}, year = {2023}, pdf = {2023.King.Implementing_a_Solver-Independent_SMT-LIB2_Parser-Interpreter_and_Code-Generator_for_JavaSMT_with_Subsequent_Evaluation.pdf}, keyword = {JavaSMT, SMT-LIB2, SMT, CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, venue = {LMU Munich}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, }
2022
-
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 -
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 -
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 -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
Program Transformation in CPAchecker: Design and Implementation of a Source-Respecting Translation from Control-Flow Automata to C Code.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2022.
Keyword(s):
CPAchecker
BibTeX Entry
@misc{CimbalnikCfaExport, author = {Klara Cimbalnik}, title = {Program Transformation in \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}, } -
Developing a Verifier Based on Parallel Portfolio with CoVeriTeam.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2022.
Keyword(s):
Benchmarking
PDF
Presentation
BibTeX Entry
@misc{KleinertParPortfolioCoVeriTeam, author = {Tobias Kleinert}, title = {Developing a Verifier Based on Parallel Portfolio with \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}, } -
Cgroups v2 Support for BenchExec.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2022.
Keyword(s):
Benchmarking
PDF
Presentation
BibTeX Entry
@misc{GlosterCgroupsV2, author = {Robin Gloster}, title = {Cgroups v2 Support for \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}, }
2021
-
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, }
2020
-
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}, } -
Software Verification with Numerical Domains in CPAchecker.
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}, } -
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}, } -
Implementierung und Evaluation von einfacher Schleifenabstraktion für das CPAchecker-Framework.
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}, } -
Improve Analysis of Java Programs in CPAchecker.
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}, } -
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}, } -
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 CPAchecker.
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}, } -
Domain Types for Predicate Analysis in CPAchecker.
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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 -
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}, } -
A Language Server and IDE Plugin for CPAchecker.
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, }
2019
-
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, }
2018
-
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.}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, }
2017
-
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ü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) -
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}, } -
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}, } -
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}, } -
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}, } -
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}, }
2016
-
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, }
2015
-
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}, } -
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}, } -
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}, } -
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}, }
2014
-
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}, } -
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}, } -
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}, }
2013
-
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}, } -
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}, }
2012
-
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}, } -
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)}, } -
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 = {}, } -
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}, } -
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
2011
-
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 -
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}, }
2010
-
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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
2009
-
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}, }
2008
-
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}, }
2007
-
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}, }
2006
-
Integrating Shape Analysis into the Model Checker Blast.
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
2005
-
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}, }
2004
-
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}, }
2003
-
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}, }
2002
-
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}, }
2000
-
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
1998
-
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}, }
Disclaimer:
This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.