Falsification of Hybrid Systems Using Adaptive Probabilistic Search.

Publications of year 2019

Books and proceedings

  1. Dirk Beyer and Chantal Keller, editors. Proceedings of the 13th International Conference on Tests and Proofs (TAP). LNCS 11823, 2019. Springer. doi:10.1007/978-3-030-31157-5 Link to this entry Publisher's Version PDF Supplement
    BibTeX Entry
    @proceedings{TAP19, title = {Proceedings of the 13th International Conference on Tests and Proofs (TAP)}, editor = {Dirk Beyer and Chantal Keller}, year = {2019}, series = {LNCS~11823}, publisher = {Springer}, isbn = {978-3-030-31156-8}, doi = {10.1007/978-3-030-31157-5}, sha256 = {}, url = {https://tap.sosy-lab.org/2019/}, pdf = {https://doi.org/10.1007/978-3-030-31157-5}, }
  2. Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen, editors. Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part 3. LNCS 11429, 2019. Springer. doi:10.1007/978-3-030-17502-3 Link to this entry Publisher's Version PDF Supplement
    BibTeX Entry
    @proceedings{TOOLympics19, title = {Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part 3}, editor = {Dirk Beyer and Marieke Huisman and Fabrice Kordon and Bernhard Steffen}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, isbn = {978-3-030-17501-6}, doi = {10.1007/978-3-030-17502-3}, sha256 = {}, url = {https://tacas.info/toolympics.php}, pdf = {https://doi.org/10.1007/978-3-030-17502-3}, }

Articles in journal or book chapters

  1. Dirk Beyer, Stefan Löwe, and Philipp Wendler. Reliable Benchmarking: Requirements and Solutions. International Journal on Software Tools for Technology Transfer (STTT), 21(1):1-29, 2019. doi:10.1007/s10009-017-0469-y Link to this entry Keyword(s): Benchmarking Publisher's Version PDF Presentation Supplement
    Abstract
    Benchmarking is a widely used method in experimental computer science, in particular, for the comparative evaluation of tools and algorithms. As a consequence, a number of questions need to be answered in order to ensure proper benchmarking, resource measurement, and presentation of results, all of which is essential for researchers, tool developers, and users, as well as for tool competitions. We identify a set of requirements that are indispensable for reliable benchmarking and resource measurement of time and memory usage of automatic solvers, verifiers, and similar tools, and discuss limitations of existing methods and benchmarking tools. Fulfilling these requirements in a benchmarking framework can (on Linux systems) currently only be done by using the cgroup and namespace features of the kernel. We developed BenchExec, a ready-to-use, tool-independent, and open-source implementation of a benchmarking framework that fulfills all presented requirements, making reliable benchmarking and resource measurement easy. Our framework is able to work with a wide range of different tools, has proven its reliability and usefulness in the International Competition on Software Verification, and is used by several research groups worldwide to ensure reliable benchmarking. Finally, we present guidelines on how to present measurement results in a scientifically valid and comprehensible way.
    BibTeX Entry
    @article{Benchmarking-STTT, author = {Dirk Beyer and Stefan L{\"o}we and Philipp Wendler}, title = {Reliable Benchmarking: {R}equirements and Solutions}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, volume = {21}, number = {1}, pages = {1--29}, year = {2019}, doi = {10.1007/s10009-017-0469-y}, sha256 = {a50fbc212af394b32166d6354f986e7b1d5bc87220bdc50df899d6a46fedf33c}, url = {https://www.sosy-lab.org/research/benchmarking/}, presentation = {https://www.sosy-lab.org/research/prs/Current_ReliableBenchmarking.pdf}, abstract = {Benchmarking is a widely used method in experimental computer science, in particular, for the comparative evaluation of tools and algorithms. As a consequence, a number of questions need to be answered in order to ensure proper benchmarking, resource measurement, and presentation of results, all of which is essential for researchers, tool developers, and users, as well as for tool competitions. We identify a set of requirements that are indispensable for reliable benchmarking and resource measurement of time and memory usage of automatic solvers, verifiers, and similar tools, and discuss limitations of existing methods and benchmarking tools. Fulfilling these requirements in a benchmarking framework can (on Linux systems) currently only be done by using the cgroup and namespace features of the kernel. We developed BenchExec, a ready-to-use, tool-independent, and open-source implementation of a benchmarking framework that fulfills all presented requirements, making reliable benchmarking and resource measurement easy. Our framework is able to work with a wide range of different tools, has proven its reliability and usefulness in the International Competition on Software Verification, and is used by several research groups worldwide to ensure reliable benchmarking. Finally, we present guidelines on how to present measurement results in a scientifically valid and comprehensible way.}, keyword = {Benchmarking}, _pdf = {https://www.sosy-lab.org/research/pub/2019-STTT.Reliable_Benchmarking_Requirements_and_Solutions.pdf}, annote = {Publication appeared first online in November 2017
    BenchExec is available at: https://github.com/sosy-lab/benchexec}, }
    Additional Infos
    Publication appeared first online in November 2017
    BenchExec is available at: https://github.com/sosy-lab/benchexec

Articles in conference or workshop proceedings

  1. Dirk Beyer and Thomas Lemberger. TestCov: Robust Test-Suite Execution and Coverage Measurement. In Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering (ASE 2019, San Diego, CA, USA, November 11-15), pages 1074-1077, 2019. IEEE. doi:10.1109/ASE.2019.00105 Link to this entry Keyword(s): DFG-COOP, Software Testing Publisher's Version PDF Presentation
    BibTeX Entry
    @inproceedings{ASE19, author = {Dirk Beyer and Thomas Lemberger}, title = {{T}est{C}ov: Robust Test-Suite Execution and Coverage Measurement}, booktitle = {Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering (ASE 2019, San Diego, CA, USA, November 11-15)}, pages = {1074-1077}, year = {2019}, publisher = {IEEE}, doi = {10.1109/ASE.2019.00105}, sha256 = {}, pdf = {https://www.sosy-lab.org/research/pub/2019-ASE.TestCov_Robust_Test-Suite_Execution_and_Coverage_Measurement.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2019-11-12_ASE19_TestCov_Thomas_Lemberger.pdf}, keyword = {DFG-COOP,Software Testing}, isbnnote = {978-1-7281-2508-4}, }
  2. Dirk Beyer and Thomas Lemberger. Conditional Testing - Off-the-Shelf Combination of Test-Case Generators. In Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza, editors, Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA 2019, Taipei, Taiwan, October 28-31), LNCS 11781, pages 189-208, 2019. Springer. doi:10.1007/978-3-030-31784-3_11 Link to this entry Keyword(s): DFG-COOP, Software Testing Publisher's Version PDF Presentation Supplement
    BibTeX Entry
    @inproceedings{ATVA19, author = {Dirk Beyer and Thomas Lemberger}, title = {Conditional Testing - Off-the-Shelf Combination of Test-Case Generators}, booktitle = {Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA~2019, Taipei, Taiwan, October 28-31)}, editor = {Yu{-}Fang Chen and Chih{-}Hong Cheng and Javier Esparza}, pages = {189-208}, year = {2019}, series = {LNCS~11781}, publisher = {Springer}, doi = {10.1007/978-3-030-31784-3_11}, sha256 = {}, url = {https://www.sosy-lab.org/research/conditional-testing/}, pdf = {https://www.sosy-lab.org/research/pub/2019-ATVA.Conditional_Testing_Off-the-Shelf_Combination_of_Test-Case_Generators.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2019-10-29_ATVA19_Conditional_Testing_Thomas_Lemberger.pdf}, keyword = {DFG-COOP,Software Testing}, }
  3. Dirk Beyer. A Data Set of Program Invariants and Error Paths. In Proceedings of the 2019 IEEE/ACM 16th International Conference on Mining Software Repositories (MSR 2019, Montreal, Canada, May 26-27), pages 111-115, 2019. IEEE. doi:10.1109/MSR.2019.00026 Link to this entry Publisher's Version PDF Supplement
    BibTeX Entry
    @inproceedings{MSR19, author = {Dirk Beyer}, title = {A Data Set of Program Invariants and Error Paths}, booktitle = {Proceedings of the 2019 IEEE/ACM 16th International Conference on Mining Software Repositories (MSR~2019, Montreal, Canada, May 26-27)}, pages = {111-115}, year = {2019}, publisher = {IEEE}, doi = {10.1109/MSR.2019.00026}, sha256 = {}, url = {https://doi.org/10.5281/zenodo.2559175}, pdf = {https://www.sosy-lab.org/research/pub/2019-MSR.A_Data_Set_of_Program_Invariants_and_Error_Paths.pdf}, }
  4. Dirk Beyer. International Competition on Software Testing (Test-Comp). In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019, Prague, Czech Republic, April 6-11), part 3, LNCS 11429, pages 167-175, 2019. Springer. doi:10.1007/978-3-030-17502-3_11 Link to this entry Keyword(s): Competition on Software Testing (Test-Comp), Competition on Software Testing (Test-Comp Report), Software Testing Publisher's Version PDF Supplement
    BibTeX Entry
    @inproceedings{TACAS19c, author = {Dirk Beyer}, title = {International Competition on Software Testing (Test-Comp)}, booktitle = {Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2019, Prague, Czech Republic, April 6-11), part 3}, pages = {167-175}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, doi = {10.1007/978-3-030-17502-3_11}, sha256 = {80ba1d656e40b44c40e756010ccd32db5aad71820cd746b264f70244477fc737}, url = {https://test-comp.sosy-lab.org/2019/}, keyword = {Competition on Software Testing (Test-Comp),Competition on Software Testing (Test-Comp Report),Software Testing}, }
  5. Dirk Beyer. Automatic Verification of C and Java Programs: SV-COMP 2019. In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019, Prague, Czech Republic, April 6-11), part 3, LNCS 11429, pages 133-155, 2019. Springer. doi:10.1007/978-3-030-17502-3_9 Link to this entry Keyword(s): Competition on Software Verification (SV-COMP), Competition on Software Verification (SV-COMP Report), Software Model Checking Publisher's Version PDF Supplement
    BibTeX Entry
    @inproceedings{TACAS19b, author = {Dirk Beyer}, title = {Automatic Verification of {C} and Java Programs: {SV-COMP} 2019}, booktitle = {Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2019, Prague, Czech Republic, April 6-11), part 3}, pages = {133-155}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, doi = {10.1007/978-3-030-17502-3_9}, sha256 = {3ded73753689c5a68001ad42c27c2a0071f0d13546ffb8c4780891a16d9cabc7}, url = {https://sv-comp.sosy-lab.org/2019/}, keyword = {Competition on Software Verification (SV-COMP),Competition on Software Verification (SV-COMP Report),Software Model Checking}, }
  6. E. Bartocci, D. Beyer, P. E. Black, G. Fedyukovich, H. Garavel, A. Hartmanns, M. Huisman, F. Kordon, J. Nagele, M. Sighireanu, B. Steffen, M. Suda, G. Sutcliffe, T. Weber, and A. Yamada. TOOLympics 2019: An Overview of Competitions in Formal Methods. In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019, Prague, Czech Republic, April 6-11), part 3, LNCS 11429, pages 3-24, 2019. Springer. doi:10.1007/978-3-030-17502-3_1 Link to this entry Publisher's Version PDF Supplement
    BibTeX Entry
    @inproceedings{TACAS19a, author = {E.~Bartocci and D.~Beyer and P.~E.~Black and G.~Fedyukovich and H.~Garavel and A.~Hartmanns and M.~Huisman and F.~Kordon and J.~Nagele and M.~Sighireanu and B.~Steffen and M.~Suda and G.~Sutcliffe and T.~Weber and A.~Yamada}, title = {{TOOLympics} 2019: An Overview of Competitions in Formal Methods}, booktitle = {Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2019, Prague, Czech Republic, April 6-11), part 3}, pages = {3-24}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, doi = {10.1007/978-3-030-17502-3_1}, sha256 = {1659009075a34066ea759286b122c9d96c6f21f6a23479fff2b8847c88482a71}, url = {https://tacas.info/toolympics.php}, }
  7. Dirk Beyer and Marie-Christine Jakobs. CoVeriTest: Cooperative Verifier-Based Testing. In Proceedings of the 22nd International Conference on Fundamental Approaches to Software Engineering (FASE 2019, Prague, Czech Republic, April 6-11), LNCS 11424, pages 389-408, 2019. Springer. doi:10.1007/978-3-030-16722-6_23 Link to this entry Keyword(s): CPAchecker, Software Model Checking, Software Testing Publisher's Version PDF Supplement
    BibTeX Entry
    @inproceedings{FASE19, author = {Dirk Beyer and Marie-Christine Jakobs}, title = {CoVeriTest: Cooperative Verifier-Based Testing}, booktitle = {Proceedings of the 22nd International Conference on Fundamental Approaches to Software Engineering (FASE~2019, Prague, Czech Republic, April 6-11)}, pages = {389-408}, year = {2019}, series = {LNCS~11424}, publisher = {Springer}, doi = {10.1007/978-3-030-16722-6_23}, sha256 = {ee64749fba4796ed79cecfaa500731ef2ac5d5e795770c44b1e7ad358f955398}, url = {https://www.sosy-lab.org/research/coop-testgen/}, keyword = {CPAchecker,Software Model Checking,Software Testing}, }
  8. Dirk Beyer, Marie-Christine Jakobs, Thomas Lemberger, and Heike Wehrheim. Combining Verifiers in Conditional Model Checking via Reducers. In S. Becker, I. Bogicevic, G. Herzwurm, and S. Wagner, editors, Proceedings of the Conference on Software Engineering and Software Management (SE/SWM 2019, Stuttgart, Germany, February 18-22), LNI P-292, pages 151-152, 2019. GI. doi:10.18420/se2019-46 Link to this entry Publisher's Version PDF Presentation
    Abstract
    Software verification received lots of attention in the past two decades. Nonetheless, it remains an extremely difficult problem. Some verification tasks cannot be solved automatically by any of today’s verifiers. To still verify such tasks, one can combine the strengths of different verifiers. A promising approach to create combinations is conditional model checking (CMC). In CMC, the first verifier outputs a condition that describes the parts of the program state space that it successfully verified, and the next verifier uses that condition to steer its exploration towards the unverified state space. Despite the benefits of CMC, only few verifiers can handle conditions. To overcome this problem, we propose an automatic plug-and-play extension for verifiers. Instead of modifying verifiers, we suggest to add a preprocessor: the reducer. The reducer takes the condition and the original program and computes a residual program that encodes the unverified state space in program code. We developed one such reducer and use it to integrate existing verifiers and test-case generators into the CMC process. Our experiments show that we can solve many additional verification tasks with this reducer-based construction.
    BibTeX Entry
    @inproceedings{SE19, author = {Dirk Beyer and Marie-Christine Jakobs and Thomas Lemberger and Heike Wehrheim}, title = {Combining Verifiers in Conditional Model Checking via Reducers}, booktitle = {Proceedings of the Conference on Software Engineering and Software Management (SE/SWM~2019, Stuttgart, Germany, February 18-22)}, editor = {S.~Becker and I.~Bogicevic and G.~Herzwurm and S.~Wagner}, pages = {151--152}, year = {2019}, series = {{LNI}~P-292}, publisher = {{GI}}, doi = {10.18420/se2019-46}, sha256 = {}, pdf = {https://www.sosy-lab.org/research/pub/2019-SE.Combining_Verifiers_in_Conditional_Model_Checking_via_Reducers.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2019-02-22_SE19_CombiningVerifiersInConditionalModelChecking_Marie.pdf}, abstract = {Software verification received lots of attention in the past two decades. Nonetheless, it remains an extremely difficult problem. Some verification tasks cannot be solved automatically by any of today’s verifiers. To still verify such tasks, one can combine the strengths of different verifiers. A promising approach to create combinations is conditional model checking (CMC). In CMC, the first verifier outputs a condition that describes the parts of the program state space that it successfully verified, and the next verifier uses that condition to steer its exploration towards the unverified state space. Despite the benefits of CMC, only few verifiers can handle conditions. To overcome this problem, we propose an automatic plug-and-play extension for verifiers. Instead of modifying verifiers, we suggest to add a preprocessor: the reducer. The reducer takes the condition and the original program and computes a residual program that encodes the unverified state space in program code. We developed one such reducer and use it to integrate existing verifiers and test-case generators into the CMC process. Our experiments show that we can solve many additional verification tasks with this reducer-based construction.}, }
  9. G. Ernst, S. Sedwards, Z. Zhang, and I. Hasuo. Fast Falsification of Hybrid Systems using Probabilistically Adaptive Input. In Proc. of Quantitative Evaluation of Systems (QEST), 2019. Springer. Link to this entry To appear. PDF
    BibTeX Entry
    @inproceedings{ernst:qest2019, author = {G. Ernst and S. Sedwards and Z. Zhang and I. Hasuo}, title = {Fast Falsification of Hybrid Systems using Probabilistically Adaptive Input}, booktitle = {Proc. of Quantitative Evaluation of Systems (QEST)}, year = {2019}, publisher = {Springer}, pdf = {https://arxiv.org/abs/1812.04159}, note = {To appear.}, }
  10. G. Ernst and T. Murray. SecCSL: Security Concurrent Separation Logic. In Proc. of Computer Aided Verification (CAV), LNCS, pages 208-230, 2019. Springer. Link to this entry PDF
    BibTeX Entry
    @inproceedings{ernst:cav2019, author = {G. Ernst and T. Murray}, title = {{SecCSL: Security Concurrent Separation Logic}}, booktitle = {Proc. of Computer Aided Verification (CAV)}, volume = {11562}, pages = {208--230}, year = {2019}, series = {LNCS}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2019-CAV.SecCSL_Security_Concurrent_Separation_Logic.pdf}, }
  11. G. Ernst, P. Arcaini, A. Donze, G. Fainekos, L. Mathesen, G. Pedrielli, S. Yaghoubi, Y. Yamagata, and Z. Zhang. ARCH-COMP19 Category Report: Results on the Falsification Benchmarks. In Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH), EPiC, pages 129-140, 2019. EasyChair. doi:10.29007/68dk Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{ernst:arch2019, author = {G. Ernst and P. Arcaini and A. Donze and G. Fainekos and L. Mathesen and G. Pedrielli and S. Yaghoubi and Y. Yamagata and Z. Zhang}, title = {{ARCH-COMP19 Category Report: Results on the Falsification Benchmarks}}, booktitle = {Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH)}, volume = {61}, pages = {129--140}, year = {2019}, series = {EPiC}, publisher = {EasyChair}, doi = {10.29007/68dk}, sha256 = {}, pdf = {https://www.sosy-lab.org/research/pub/2019-ARCH.Category_Report_Falsification.pdf}, }
  12. G. Ernst, M. Huisman, W. Mostowski, and M. Ulbrich. VerifyThis - Verification Competition with a Human Factor. In Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, 2019. Springer. Link to this entry PDF
    BibTeX Entry
    @inproceedings{ernst:toolympics2019, author = {G. Ernst and M. Huisman and W. Mostowski and M. Ulbrich}, title = {{VerifyThis -- Verification Competition with a Human Factor}}, booktitle = {Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, volume = {11429}, year = {2019}, series = {LNCS}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2019-TACAS.VerifyThis-Verification_Competition_with_a_Human_Factor.pdf}, }
  13. Rolf Hennicker, Alexander Knapp, Alexandre Madeira, and Felix Mindt. Behavioural and Abstractor Specifications for a Dynamic Logic with Binders and Silent Transitions. In Proceedings of the International Workshop on Data Learning and Inference (DALI 2019, San Sebastian, Spain, September 03-06), LCNS, 2019. Springer. Link to this entry (to appear) PDF
    Abstract
    We extend dynamic logic with binders (for state variables) by distinguishing between observable and silent transitions. This differentiation gives rise to two kinds of observational interpretations of the logic: abstractor and behavioural specifications. Abstractor specifications relax the standard model class semantics of a specification by considering its closure under weak bisimulation. Behavioural specifications, however, rely on a behavioural satisfaction relation which relaxes the interpretation of state variables and the satisfaction of modal formulas ⟨α⟩φ and [α]φ by abstracting from silent transitions. A formal relation between abstractor and behavioural specifications is provided which shows that both coincide semantically under mild conditions. For the proof we instantiate the previously introduced concept of a behaviour-abstractor framework to the case of dynamic logic with binders and silent transitions.
    BibTeX Entry
    @inproceedings{DaLi19, author = {Rolf Hennicker and Alexander Knapp and Alexandre Madeira and Felix Mindt}, title = {Behavioural and Abstractor Specifications for a Dynamic Logic with Binders and Silent Transitions}, booktitle = {Proceedings of the International Workshop on Data Learning and Inference (DALI~2019, San Sebastian, Spain, September 03-06)}, year = {2019}, series = {{LCNS}}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2019-DALI.Behavioural_and_Abstractor_Specifications_for_a_Dynamic_Logic_with_Binders_and_Silent_Transitions.pdf}, abstract = {We extend dynamic logic with binders (for state variables) by distinguishing between observable and silent transitions. This differentiation gives rise to two kinds of observational interpretations of the logic: abstractor and behavioural specifications. Abstractor specifications relax the standard model class semantics of a specification by considering its closure under weak bisimulation. Behavioural specifications, however, rely on a behavioural satisfaction relation which relaxes the interpretation of state variables and the satisfaction of modal formulas ⟨α⟩φ and [α]φ by abstracting from silent transitions. A formal relation between abstractor and behavioural specifications is provided which shows that both coincide semantically under mild conditions. For the proof we instantiate the previously introduced concept of a behaviour-abstractor framework to the case of dynamic logic with binders and silent transitions.}, note = {(to appear)}, }

Internal reports

  1. Dirk Beyer and Matthias Dangl. Software Verification with PDR: Implementation and Empirical Evaluation of the State of the Art. Technical report 1908.06271, arXiv/CoRR, August 2019. Link to this entry PDF
    BibTeX Entry
    @techreport{TechReport19b, author = {Dirk Beyer and Matthias Dangl}, title = {Software Verification with PDR: Implementation and Empirical Evaluation of the State of the Art}, number = {1908.06271}, year = {2019}, pdf = {https://arxiv.org/abs/1908.06271}, institution = {arXiv/CoRR}, month = {August}, }
  2. Dirk Beyer and Heike Wehrheim. Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework. Technical report 1905.08505, arXiv/CoRR, May 2019. Link to this entry PDF
    BibTeX Entry
    @techreport{TechReport19a, author = {Dirk Beyer and Heike Wehrheim}, title = {Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework}, number = {1905.08505}, year = {2019}, pdf = {https://arxiv.org/abs/1905.08505}, institution = {arXiv/CoRR}, month = {May}, }

Theses and projects (PhD, MSc, BSc, Project)

  1. Alexander Koos. Implementation and Evaluation of a Framework for Canonization and Caching of SMT Formulae. Master's Thesis, LMU Munich, Software Systems Lab, 2019. Link to this entry 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}, }
  2. Stephan Holzner. Design und Implementierung einer parallelen BDD-Bibliothek. Master's Thesis, LMU Munich, Software Systems Lab, 2019. Link to this entry 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}, }
  3. Michael Maier. SMT-Based Verification of ECMAScript Programs in CPAchecker. Master's Thesis, LMU Munich, Software Systems Lab, 2019. Link to this entry 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}, }
  4. Mirjam Trapp. Heuristics for Effective Predicate Refinement in CPAchecker. Master's Thesis, LMU Munich, Software Systems Lab, 2019. Link to this entry 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}, }
  5. Thomas Bunk. LTL Software Model Checking in CPAchecker. Master's Thesis, LMU Munich, Software Systems Lab, 2019. Link to this entry 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}, }
  6. Maximilian Hailer. Measuring and Optimizing Energy Consumption of Verification Work on Clusters. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019. Link to this entry 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}, }
  7. Daniel Baier. Integration des SMT-Solvers Boolector in das Framework JavaSMT und Evaluation mit CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019. Link to this entry 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}, }
  8. Laura Bschor. Modern Architecture and Improved UI for Tables of BenchExec. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019. Link to this entry 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}, }
  9. Maximilian Wiesholler. Correctness Witness Validation using Predicate Analysis. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019. Link to this entry 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}, }
  10. Krutav Shah. Counterexample-Guided Abstraction Refinement for Interval Domain. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019. Link to this entry 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}, }
  11. Raphael Hagl. Hybrid Testcase Generation with CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019. Link to this entry 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}, }
  12. Andrea Kreppel. Implementation and Evaluation of Backwards Analyses in the Software-Verification Framework CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019. Link to this entry 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}, }
  13. Gregor Alexandru. Specifying Loops with Contracts. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019. Link to this entry 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}, }
  14. Leonhard Volk. Bipartite Matching Problems: Algorithms and Properties. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019. Link to this entry
    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}, }

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.

Last modified: Sat Oct 23 23:51:13 2021