We are hiring new doctoral researchers, student research assistants, and tutors. Apply now!
2 papers accepted at ASE 2024: BenchCloud and CoVeriTeam GUI

Publications of year 2020

Books and proceedings
  1. Dirk Beyer and Damien Zufferey, editors. Proceedings of the 21st International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). LNCS 11990, 2020. Springer. doi:10.1007/978-3-030-39322-9 Link to this entry Publisher's Version PDF Supplement
    BibTeX Entry
    @proceedings{VMCAI20, title = {Proceedings of the 21st International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)}, editor = {Dirk Beyer and Damien Zufferey}, year = {2020}, series = {LNCS~11990}, publisher = {Springer}, isbn = {978-3-030-39321-2}, doi = {10.1007/978-3-030-39322-9}, sha256 = {}, url = {https://popl20.sigplan.org/home/VMCAI-2020}, pdf = {https://doi.org/10.1007/978-3-030-39322-9}, }

Articles in journal or book chapters
  1. Dirk Beyer and Marieke Huisman. Tools for the Construction and Analysis of Systems (Intro). International Journal on Software Tools for Technology Transfer (STTT), 22(6):685-687, 2020. doi:10.1007/s10009-020-00581-0 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @article{Intro-TACAS18-STTT, author = {Dirk Beyer and Marieke Huisman}, title = {Tools for the Construction and Analysis of Systems (Intro)}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, volume = {22}, number = {6}, pages = {685-687}, year = {2020}, doi = {10.1007/s10009-020-00581-0}, sha256 = {467e6c9c70fd0c0728a8abed5d9162a1467a906e79d367a8a44dd102e8dc0de6}, url = {}, pdf = {}, presentation = {}, abstract = {}, keyword = {}, issn = {1433-2787}, }
  2. Dirk Beyer and Marieke Huisman. Selected and Extended Papers from TACAS 2018: Preface. Journal of Automated Reasoning, 64(7):1331-1332, 2020. doi:10.1007/s10817-020-09575-8 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @article{Intro-TACAS18-JAR, author = {Dirk Beyer and Marieke Huisman}, title = {Selected and Extended Papers from {TACAS} 2018: Preface}, journal = {Journal of Automated Reasoning}, volume = {64}, number = {7}, pages = {1331-1332}, year = {2020}, doi = {10.1007/s10817-020-09575-8}, sha256 = {252d10dfb4cd4c93db83e431938420d0927be076e598c176db1ea85514a5ba0a}, url = {}, pdf = {}, presentation = {}, abstract = {}, keyword = {}, }
  3. Gidon Ernst. A Complete Approach to Loop Verification with Invariants and Summaries. arXiv preprint arXiv:2010.05812, 2020. Link to this entry
    BibTeX Entry
    @article{ernst:loops2020, author = {Gidon Ernst}, title = {A Complete Approach to Loop Verification with Invariants and Summaries}, journal = {arXiv preprint arXiv:2010.05812}, year = {2020}, }
  4. Thomas Lemberger. Plain random test generation with PRTest. International Journal on Software Tools for Technology Transfer (STTT), 2020. Springer. doi:10.1007/s10009-020-00568-x Link to this entry Keyword(s): Software Testing Publisher's Version PDF Presentation
    Abstract
    Automatic test-suite generation tools are often complex and their behavior is not predictable. To provide a minimum baseline that test-suite generators should be able to surpass, we present PRTest, a random black-box test-suite generator for C programs: To create a test, PRTest natively executes the program under test and creates a new, random test value whenever an input value is required. After execution, PRTest checks whether any new program branches were covered and, if this is the case, the created test is added to the test suite. This way, tests are rapidly created either until a crash is found, or until the user aborts the creation. While this naive mechanism is not competitive with more sophisticated, state-of-the-art test-suite generation tools, it is able to provide a good baseline for Test-Comp and a fast alternative for automatic test-suite generation for programs with simple control flow. PRTest is publicly available and open source.
    BibTeX Entry
    @article{PRTEST19, author = {Thomas Lemberger}, title = {Plain random test generation with {PRTest}}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, volume = {}, number = {}, pages = {}, year = {2020}, publisher = {Springer}, doi = {10.1007/s10009-020-00568-x}, sha256 = {2e5ae7091b6adb758c123dfe62d3fab57203f930883539beb20f6e91391ebc77}, pdf = {https://www.sosy-lab.org/research/pub/2020-STTT.Plain_random_test_generation_with_PRTest.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2019-04-06_TestComp19_PRTest_Thomas.pdf}, abstract = {Automatic test-suite generation tools are often complex and their behavior is not predictable. To provide a minimum baseline that test-suite generators should be able to surpass, we present PRTest, a random black-box test-suite generator for C programs: To create a test, PRTest natively executes the program under test and creates a new, random test value whenever an input value is required. After execution, PRTest checks whether any new program branches were covered and, if this is the case, the created test is added to the test suite. This way, tests are rapidly created either until a crash is found, or until the user aborts the creation. While this naive mechanism is not competitive with more sophisticated, state-of-the-art test-suite generation tools, it is able to provide a good baseline for Test-Comp and a fast alternative for automatic test-suite generation for programs with simple control flow. PRTest is publicly available and open source.}, keyword = {Software Testing}, annote = {Publication appeared first online in July 2020.<BR/> PRTest is available at <a href="https://gitlab.com/sosy-lab/software/prtest"> https://gitlab.com/sosy-lab/software/prtest</a>}, }
    Additional Infos
    Publication appeared first online in July 2020.
    PRTest is available at https://gitlab.com/sosy-lab/software/prtest
  5. Rocco De Nicola, Stefan Jähnichen, and Martin Wirsing. Rigorous engineering of collective adaptive systems: special section. Int. J. Softw. Tools Technol. Transf., 22(4):389-397, 2020. doi:10.1007/s10009-020-00565-0 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @article{DBLP:journals/sttt/NicolaJW20, author = {Rocco De Nicola and Stefan J{\"{a}}hnichen and Martin Wirsing}, title = {Rigorous engineering of collective adaptive systems: special section}, journal = {Int. J. Softw. Tools Technol. Transf.}, volume = {22}, number = {4}, pages = {389--397}, year = {2020}, doi = {10.1007/s10009-020-00565-0}, }

Articles in conference or workshop proceedings
  1. Dirk Beyer and Karlheinz Friedberger. Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization. In P. Devanbu, M. Cohen, and T. Zimmermann, editors, Proceedings of the 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2020, Virtual Event, USA, November 8-13), pages 50-62, 2020. ACM. doi:10.1145/3368089.3409718 Link to this entry Keyword(s): CPAchecker, Software Model Checking Funding: DFG-CONVEY Publisher's Version PDF Supplement
    Artifact(s)
    BibTeX Entry
    @inproceedings{FSE20, author = {Dirk Beyer and Karlheinz Friedberger}, title = {Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization}, booktitle = {Proceedings of the 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE~2020, Virtual Event, USA, November 8-13)}, editor = {P.~Devanbu and M.~Cohen and T.~Zimmermann}, pages = {50-62}, year = {2020}, publisher = {ACM}, doi = {10.1145/3368089.3409718}, url = {https://cpachecker.sosy-lab.org}, keyword = {CPAchecker,Software Model Checking}, _sha256 = {36dc2a423425ee8bec03f0f4073e04f9121d299cc475e27190828e8276e00cb8}, artifact = {10.5281/zenodo.4024268}, funding = {DFG-CONVEY}, fundingid = {378803395}, }
  2. Dirk Beyer and Karlheinz Friedberger. Violation Witnesses and Result Validation for Multi-Threaded Programs. In T. Margaria and B. Steffen, editors, Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2020, Rhodos, Greece, October 26-30), part 1, LNCS 12476, pages 449-470, 2020. Springer. doi:10.1007/978-3-030-61362-4_26 Link to this entry Keyword(s): CPAchecker, Software Model Checking, Witness-Based Validation, Witness-Based Validation (main) Funding: DFG-CONVEY Publisher's Version PDF Presentation Supplement
    BibTeX Entry
    @inproceedings{ISoLA20c, author = {Dirk Beyer and Karlheinz Friedberger}, title = {Violation Witnesses and Result Validation for Multi-Threaded Programs}, booktitle = {Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2020, Rhodos, Greece, October 26-30), part~1}, editor = {T.~Margaria and B.~Steffen}, pages = {449-470}, year = {2020}, series = {LNCS~12476}, publisher = {Springer}, doi = {10.1007/978-3-030-61362-4_26}, sha256 = {65fc5325c4e77a80d8e47f9c0e7f0ac02379bfa15dcd9fb54d6587185b8efd77}, url = {https://www.sosy-lab.org/research/witnesses-concurrency/}, presentation = {https://www.sosy-lab.org/research/prs/2021-10-25_ISOLA21_ValidationMultiThreaded_Dirk.pdf}, abstract = {}, keyword = {CPAchecker,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)}, funding = {DFG-CONVEY}, }
  3. Dirk Beyer and Sudeep Kanav. An Interface Theory for Program Verification. In T. Margaria and B. Steffen, editors, Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2020, Rhodos, Greece, October 26-30), part 1, LNCS 12476, pages 168-186, 2020. Springer. doi:10.1007/978-3-030-61362-4_9 Link to this entry Keyword(s): CPAchecker, Software Model Checking, Interfaces for Component-Based Design Funding: DFG-CONVEY Publisher's Version PDF Presentation
    BibTeX Entry
    @inproceedings{ISoLA20b, author = {Dirk Beyer and Sudeep Kanav}, title = {An Interface Theory for Program Verification}, booktitle = {Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2020, Rhodos, Greece, October 26-30), part~1}, editor = {T.~Margaria and B.~Steffen}, pages = {168-186}, year = {2020}, series = {LNCS~12476}, publisher = {Springer}, doi = {10.1007/978-3-030-61362-4_9}, sha256 = {f15159da0e648a25e57c769639c989e68cd3407bfad10db5ee1dc25e1d2fd672}, url = {}, presentation = {https://www.sosy-lab.org/research/prs/2021-10-29_ISOLA21_VerificationInterfaces_Dirk.pdf}, abstract = {}, keyword = {CPAchecker,Software Model Checking,Interfaces for Component-Based Design}, funding = {DFG-CONVEY}, }
  4. Dirk Beyer and Heike Wehrheim. Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework. In T. Margaria and B. Steffen, editors, Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2020, Rhodos, Greece, October 26-30), part 1, LNCS 12476, pages 143-167, 2020. Springer. doi:10.1007/978-3-030-61362-4_8 Link to this entry Keyword(s): Software Model Checking, Cooperative Verification Funding: DFG-COOP Publisher's Version PDF Presentation
    BibTeX Entry
    @inproceedings{ISoLA20a, author = {Dirk Beyer and Heike Wehrheim}, title = {Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework}, booktitle = {Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2020, Rhodos, Greece, October 26-30), part~1}, editor = {T.~Margaria and B.~Steffen}, pages = {143-167}, year = {2020}, series = {LNCS~12476}, publisher = {Springer}, doi = {10.1007/978-3-030-61362-4_8}, sha256 = {86dbfb5ee4875582566bdb5d44750cc935614c11c09627295cc3ff123115a75b}, url = {}, presentation = {https://www.sosy-lab.org/research/prs/2021-10-29_ISOLA21_VerificationArtifacts_Dirk.pdf}, abstract = {}, keyword = {Software Model Checking,Cooperative Verification}, funding = {DFG-COOP}, fundingid = {418257054}, }
  5. Dirk Beyer, Marie-Christine Jakobs, and Thomas Lemberger. Difference Verification with Conditions. In F. d. Boer and A. Cerone, editors, Proceedings of the 18th International Conference on Software Engineering and Formal Methods (SEFM 2020, Virtual, Netherlands, September 14-18), LNCS 12310, pages 133-154, 2020. Springer. doi:10.1007/978-3-030-58768-0_8 Link to this entry Keyword(s): CPAchecker, Software Model Checking Funding: DFG-COOP, DFG-CONVEY Publisher's Version PDF Presentation Video Supplement
    Abstract
    Modern software-verification tools need to support development processes that involve frequent changes. Existing approaches for incremental verification hard-code specific verification techniques. Some of the approaches must be tightly intertwined with the development process. To solve this open problem, we present the concept of difference verification with conditions. Difference verification with conditions is independent from any specific verification technique and can be integrated in software projects at any time. It first applies a change analysis that detects which parts of a software were changed between revisions and encodes that information in a condition. Based on this condition, an off-the-shelf verifier is used to verify only those parts of the software that are influenced by the changes. As a proof of concept, we propose a simple, syntax-based change analysis and use difference verification with conditions with three off-the-shelf verifiers. An extensive evaluation shows the competitiveness of difference verification with conditions.
    BibTeX Entry
    @inproceedings{SEFM20b, author = {Dirk Beyer and Marie-Christine Jakobs and Thomas Lemberger}, title = {Difference Verification with Conditions}, booktitle = {Proceedings of the 18th International Conference on Software Engineering and Formal Methods (SEFM~2020, Virtual, Netherlands, September 14-18)}, editor = {F.~d.~Boer and A.~Cerone}, pages = {133--154}, year = {2020}, series = {LNCS~12310}, publisher = {Springer}, doi = {10.1007/978-3-030-58768-0_8}, sha256 = {8e5219da9a998b26f59013c809fbb1db6f92e3f08125fa1bfaacafcfafafef7f}, url = {https://www.sosy-lab.org/research/difference/}, presentation = {https://www.sosy-lab.org/research/prs/2020-09-17_SEFM20_DifferenceVerificationWithConditions_Thomas.pdf}, abstract = {Modern software-verification tools need to support development processes that involve frequent changes. Existing approaches for incremental verification hard-code specific verification techniques. Some of the approaches must be tightly intertwined with the development process. To solve this open problem, we present the concept of difference verification with conditions. Difference verification with conditions is independent from any specific verification technique and can be integrated in software projects at any time. It first applies a change analysis that detects which parts of a software were changed between revisions and encodes that information in a condition. Based on this condition, an off-the-shelf verifier is used to verify only those parts of the software that are influenced by the changes. As a proof of concept, we propose a simple, syntax-based change analysis and use difference verification with conditions with three off-the-shelf verifiers. An extensive evaluation shows the competitiveness of difference verification with conditions.}, keyword = {CPAchecker,Software Model Checking}, funding = {DFG-COOP,DFG-CONVEY}, isbnnote = {}, video = {https://youtu.be/dG02602c9oo}, }
  6. Dirk Beyer and Marie-Christine Jakobs. FRed: Conditional Model Checking via Reducers and Folders. In F. d. Boer and A. Cerone, editors, Proceedings of the 18th International Conference on Software Engineering and Formal Methods (SEFM 2020, Virtual, Netherlands, September 14-18), LNCS 12310, pages 113-132, 2020. Springer. doi:10.1007/978-3-030-58768-0_7 Link to this entry Keyword(s): CPAchecker, Software Model Checking Funding: DFG-COOP Publisher's Version PDF Supplement
    BibTeX Entry
    @inproceedings{SEFM20a, author = {Dirk Beyer and Marie-Christine Jakobs}, title = {{{\sc FRed}}: {C}onditional Model Checking via Reducers and Folders}, booktitle = {Proceedings of the 18th International Conference on Software Engineering and Formal Methods (SEFM~2020, Virtual, Netherlands, September 14-18)}, editor = {F.~d.~Boer and A.~Cerone}, pages = {113--132}, year = {2020}, series = {LNCS~12310}, publisher = {Springer}, doi = {10.1007/978-3-030-58768-0_7}, sha256 = {0ce35cbde24d7a9de0513b89f23a81147bf4f8d5880effd57742c7f195e0eeec}, url = {https://www.sosy-lab.org/research/fred/}, abstract = {}, keyword = {CPAchecker,Software Model Checking}, funding = {DFG-COOP}, isbnnote = {}, }
  7. Dirk Beyer and Martin Spiessl. MetaVal: Witness Validation via Verification. In S. K. Lahiri and C. Wang, editors, Proceedings of the 32nd International Conference on Computer Aided Verification (CAV 2020, Virtual, USA, July 21-24), part 2, LNCS 12225, pages 165-177, 2020. Springer. doi:10.1007/978-3-030-53291-8_10 Link to this entry Keyword(s): CPAchecker, Software Model Checking, Witness-Based Validation, Witness-Based Validation (main) Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry
    @inproceedings{CAV20, author = {Dirk Beyer and Martin Spiessl}, title = {MetaVal: {W}itness Validation via Verification}, booktitle = {Proceedings of the 32nd International Conference on Computer Aided Verification (CAV~2020, Virtual, USA, July 21-24), part 2}, editor = {S.~K.~Lahiri and C.~Wang}, pages = {165-177}, year = {2020}, series = {LNCS~12225}, publisher = {Springer}, doi = {10.1007/978-3-030-53291-8_10}, sha256 = {7431085a248c7e2cab70318096622ff19ce1124067158d08866d3f9b250df44e}, url = {https://gitlab.com/sosy-lab/software/metaval}, abstract = {}, keyword = {CPAchecker,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)}, funding = {DFG-CONVEY}, isbnnote = {978-3-030-53290-1}, }
  8. Dirk Beyer. Advances in Automatic Software Verification: SV-COMP 2020. In Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020, Dublin, Ireland, April 25-30), part 2, LNCS 12079, pages 347-367, 2020. Springer. doi:10.1007/978-3-030-45237-7_21 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
    Artifact(s)
    BibTeX Entry
    @inproceedings{TACAS20c, author = {Dirk Beyer}, title = {Advances in Automatic Software Verification: {SV-COMP 2020}}, booktitle = {Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2020, Dublin, Ireland, April 25-30), part 2}, pages = {347-367}, year = {2020}, series = {LNCS~12079}, publisher = {Springer}, doi = {10.1007/978-3-030-45237-7_21}, sha256 = {2a0cc56934c8fb6d100039b527e8c09f421ca351e4c90ec531aa2accb04504c6}, url = {https://sv-comp.sosy-lab.org/2020/}, abstract = {}, keyword = {Competition on Software Verification (SV-COMP),Competition on Software Verification (SV-COMP Report),Software Model Checking}, artifact1 = {10.5281/zenodo.3633334}, artifact2 = {10.5281/zenodo.3630205}, artifact3 = {10.5281/zenodo.3630188}, artifact4 = {10.5281/zenodo.3574420}, }
  9. Dirk Beyer and Philipp Wendler. CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering. In Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020, Dublin, Ireland, April 25-30), part 2, LNCS 12079, pages 126-133, 2020. Springer. doi:10.1007/978-3-030-45237-7_8 Link to this entry Keyword(s): Benchmarking Publisher's Version PDF Presentation Video Supplement
    Abstract
    Verification algorithms are among the most resource-intensive computation tasks. Saving energy is important for our living environment and to save cost in data centers. Yet, researchers compare the efficiency of algorithms still in terms of consumption of CPU time (or even wall time). Perhaps one reason for this is that measuring energy consumption of computational processes is not as convenient as measuring the consumed time and there is no sufficient tool support. To close this gap, we contribute CPU Energy Meter, a small tool that takes care of reading the energy values that Intel CPUs track inside the chip. In order to make energy measurements as easy as possible, we integrated CPU Energy Meter into BenchExec, a benchmarking tool that is already used by many researchers and competitions in the domain of formal methods. As evidence for usefulness, we explored the energy consumption of some state-of-the-art verifiers and report some interesting insights, for example, that energy consumption is not necessarily correlated with CPU time.
    BibTeX Entry
    @inproceedings{TACAS20b, author = {Dirk Beyer and Philipp Wendler}, title = {CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering}, booktitle = {Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2020, Dublin, Ireland, April 25-30), part 2}, pages = {126-133}, year = {2020}, series = {LNCS~12079}, publisher = {Springer}, doi = {10.1007/978-3-030-45237-7_8}, sha256 = {c5c8ad06f4b192e61799469a8fc6ca4661714aa2945e0ce07363a376ff06dcd7}, url = {https://www.sosy-lab.org/research/energy-measurement/}, presentation = {https://www.sosy-lab.org/research/prs/2021-03-31_TACAS20_CPU-Energy-Meter_Dirk.pdf}, abstract = {Verification algorithms are among the most resource-intensive computation tasks. Saving energy is important for our living environment and to save cost in data centers. Yet, researchers compare the efficiency of algorithms still in terms of consumption of CPU time (or even wall time). Perhaps one reason for this is that measuring energy consumption of computational processes is not as convenient as measuring the consumed time and there is no sufficient tool support. To close this gap, we contribute CPU Energy Meter, a small tool that takes care of reading the energy values that Intel CPUs track inside the chip. In order to make energy measurements as easy as possible, we integrated CPU Energy Meter into BenchExec, a benchmarking tool that is already used by many researchers and competitions in the domain of formal methods. As evidence for usefulness, we explored the energy consumption of some state-of-the-art verifiers and report some interesting insights, for example, that energy consumption is not necessarily correlated with CPU time.}, keyword = {Benchmarking}, video = {https://youtu.be/qzKAoBVTw2c}, }
  10. Dirk Beyer and Matthias Dangl. Software Verification with PDR: An Implementation of the State of the Art. In Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020, Dublin, Ireland, April 25-30), part 1, LNCS 12078, pages 3-21, 2020. Springer. doi:10.1007/978-3-030-45190-5_1 Link to this entry Keyword(s): Software Model Checking, CPAchecker Publisher's Version PDF Presentation Video Supplement
    BibTeX Entry
    @inproceedings{TACAS20a, author = {Dirk Beyer and Matthias Dangl}, title = {Software Verification with {PDR}: An Implementation of the State of the Art}, booktitle = {Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2020, Dublin, Ireland, April 25-30), part 1}, pages = {3-21}, year = {2020}, series = {LNCS~12078}, publisher = {Springer}, doi = {10.1007/978-3-030-45190-5_1}, sha256 = {fbd54433b42cb4411ddf6d73eb198507a6d35d8b6581b000be30aed84633e204}, url = {https://www.sosy-lab.org/research/pdr-compare/}, presentation = {https://www.sosy-lab.org/research/prs/2021-03-31_TACAS20_PDR-for-Software_Dirk.pdf}, abstract = {}, keyword = {Software Model Checking,CPAchecker}, video = {https://youtu.be/Wxqd92sdHBE}, }
  11. Dirk Beyer. Second Competition on Software Testing: Test-Comp 2020. In Proceedings of the 23rd International Conference on Fundamental Approaches to Software Engineering (FASE 2020, Dublin, Ireland, April 25-30), LNCS 12076, pages 505-519, 2020. Springer. doi:10.1007/978-3-030-45234-6_25 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
    Artifact(s)
    BibTeX Entry
    @inproceedings{FASE20, author = {Dirk Beyer}, title = {Second Competition on Software Testing: {Test-Comp 2020}}, booktitle = {Proceedings of the 23rd International Conference on Fundamental Approaches to Software Engineering (FASE~2020, Dublin, Ireland, April 25-30)}, pages = {505-519}, year = {2020}, series = {LNCS~12076}, publisher = {Springer}, doi = {10.1007/978-3-030-45234-6_25}, sha256 = {296b4caf885ae029e388c2ef8fd032f1ab55c07d5e8ea1064f2e50c08f5d6919}, url = {https://test-comp.sosy-lab.org/2020/}, abstract = {}, keyword = {Competition on Software Testing (Test-Comp),Competition on Software Testing (Test-Comp Report),Software Testing}, artifact1 = {10.5281/zenodo.3678250}, artifact2 = {10.5281/zenodo.3678264}, artifact3 = {10.5281/zenodo.3678275}, artifact4 = {10.5281/zenodo.3574420}, }
  12. Dirk Beyer and Marie-Christine Jakobs. Cooperative Test-Case Generation with Verifiers. In M. Felderer, W. Hasselbring, R. Rabiser, and R. Jung, editors, Proceedings of the Conference on Software Engineering (SE 2020, Innsbruck, Austria, February 24-28), LNI P-300, pages 107-108, 2020. GI. doi:10.18420/SE2020_31 Link to this entry Keyword(s): CPAchecker, Software Model Checking, Software Testing Publisher's Version
    BibTeX Entry
    @inproceedings{SE20, author = {Dirk Beyer and Marie-Christine Jakobs}, title = {Cooperative Test-Case Generation with Verifiers}, booktitle = {Proceedings of the Conference on Software Engineering (SE~2020, Innsbruck, Austria, February 24-28)}, editor = {M.~Felderer and W.~Hasselbring and R.~Rabiser and R.~Jung}, pages = {107--108}, year = {2020}, series = {{LNI}~P-300}, publisher = {{GI}}, doi = {10.18420/SE2020_31}, sha256 = {}, pdf = {}, presentation = {}, abstract = {}, keyword = {CPAchecker,Software Model Checking,Software Testing}, annote = {This is a summary of a <a href="https://www.sosy-lab.org/research/bib/Year/2019.html#FASE19">full article on this topic</a> that appeared in Proc. FASE 2019.}, isbnnote = {978-3-88579-694-7}, }
    Additional Infos
    This is a summary of a full article on this topic that appeared in Proc. FASE 2019.
  13. Dongge Liu, Gidon Ernst, Toby Murray, and Ben Rubinstein. Legion: Best-First Concolic Testing. In Proc. of Automated Software Engineering (ASE), pages 54-65, 2020. IEEE. Link to this entry PDF
    BibTeX Entry
    @inproceedings{ernst:ase2020, author = {Dongge Liu and Gidon Ernst and Toby Murray and Ben Rubinstein}, title = {Legion: Best-First Concolic Testing}, booktitle = {Proc. of Automated Software Engineering (ASE)}, pages = {54--65}, year = {2020}, publisher = {IEEE}, pdf = {https://arxiv.org/abs/2002.06311}, }
  14. Dongge Liu, Gidon Ernst, Toby Murray, and Benjamin Rubinstein. Legion: Best-First Concolic Testing (Competition Contribution).. In Proc. of Fundamental Approaches to Software Engineering (FASE), pages 545-549, 2020. Link to this entry
    BibTeX Entry
    @inproceedings{ernst:testcomp2020, author = {Dongge Liu and Gidon Ernst and Toby Murray and Benjamin Rubinstein}, title = {Legion: Best-First Concolic Testing (Competition Contribution).}, booktitle = {Proc. of Fundamental Approaches to Software Engineering (FASE)}, pages = {545--549}, year = {2020}, }
  15. Gidon Ernst and Lukas Rieger. Information Flow Testing of a PGP Keyserver. In Proc. of the VerifyThis Long-term Challenge 2020, pages 11-13, 2020. KIT Library. Link to this entry Technical Report.
    BibTeX Entry
    @inproceedings{ernst:vtltc2020-iftesting, author = {Gidon Ernst and Lukas Rieger}, title = {{Information Flow Testing of a PGP Keyserver}}, booktitle = {{Proc. of the VerifyThis Long-term Challenge 2020}}, pages = {11--13}, year = {2020}, publisher = {KIT Library}, note = {Technical Report.}, }
  16. Gidon Ernst, Toby Murray, and Mukesh Tiwari. Verifying the Security of a PGP Keyserver. In Proc. of the VerifyThis Long-term Challenge 2020, pages 14-16, 2020. KIT Library. Link to this entry Technical Report.
    BibTeX Entry
    @inproceedings{ernst:vtltc2020-ifverify, author = {Gidon Ernst and Toby Murray and Mukesh Tiwari}, title = {{Verifying the Security of a PGP Keyserver}}, booktitle = {{Proc. of the VerifyThis Long-term Challenge 2020}}, pages = {14--16}, year = {2020}, publisher = {KIT Library}, note = {Technical Report.}, }
  17. Gidon Ernst and others. ARCH-COMP 2020 category report: Falsification. In Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH), EPiC, pages 140-152, 2020. EasyChair. Link to this entry
    BibTeX Entry
    @inproceedings{ernst:arch2020, author = {Gidon Ernst and others}, title = {{ARCH-COMP} 2020 category report: Falsification}, booktitle = {Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH)}, volume = {74}, pages = {140--152}, year = {2020}, series = {EPiC}, publisher = {EasyChair}, }
  18. Martin Wirsing, Rocco De Nicola, and Stefan Jähnichen. Rigorous Engineering of Collective Adaptive Systems Introduction to the 3rd Track Edition. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part II, LNCS 12477, pages 161-170, 2020. Springer. doi:10.1007/978-3-030-61470-6_10 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{DBLP:conf/isola/WirsingNJ20, author = {Martin Wirsing and Rocco De Nicola and Stefan J{\"{a}}hnichen}, title = {Rigorous Engineering of Collective Adaptive Systems Introduction to the 3rd Track Edition}, booktitle = {Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part {II}}, editor = {Tiziana Margaria and Bernhard Steffen}, pages = {161--170}, year = {2020}, series = {LNCS~12477}, publisher = {Springer}, doi = {10.1007/978-3-030-61470-6\_10}, }
  19. Rolf Hennicker and Martin Wirsing. A Dynamic Logic for Systems with Predicate-Based Communication. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part II, LNCS 12477, pages 224-242, 2020. Springer. doi:10.1007/978-3-030-61470-6_14 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{DBLP:conf/isola/HennickerW20, author = {Rolf Hennicker and Martin Wirsing}, title = {A Dynamic Logic for Systems with Predicate-Based Communication}, booktitle = {Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part {II}}, editor = {Tiziana Margaria and Bernhard Steffen}, pages = {224--242}, year = {2020}, series = {LNCS~12477}, publisher = {Springer}, doi = {10.1007/978-3-030-61470-6\_14}, }

Theses and projects (PhD, MSc, BSc, Project)
  1. Moritz Beck. Solver-based Analysis of Memory Safety using Separation Logic. Master's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry Keyword(s): CPAchecker, JavaSMT, Separation Logic, Software Model Checking PDF Presentation
    BibTeX Entry
    @misc{BeckSeparationLogic, author = {Moritz Beck}, title = {Solver-based Analysis of Memory Safety using Separation Logic}, year = {2020}, pdf = {https://www.sosy-lab.org/research/msc/2020.Beck.Solver-based_Analysis_of_Memory_Safety_using_Separation_Logic.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2020-09-16_MA_SolverBasedAnalysisOfMemorySafetyUsingSeparationLogic_Beck.pdf}, keyword = {CPAchecker,JavaSMT,Separation Logic,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
  2. Martin Zehendner. Software Verification with Numerical Domains in CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry
    @misc{ZehendnerNumericalDomains, author = {Martin Zehendner}, title = {Software Verification with Numerical Domains in \textsc{CPAchecker}}, year = {2020}, keyword = {CPAchecker, Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  3. Sven Umbricht. Converting Between ACSL Annotations and Witness Invariants. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry Keyword(s): CPAchecker, Software Model Checking, ACSL PDF Presentation
    BibTeX Entry
    @misc{UmbrichtACSL, author = {Sven Umbricht}, title = {Converting Between ACSL Annotations and Witness Invariants}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Umbricht.Converting.Between.ACSL.Annotations.and.Witness.Invariants.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2021-02-10_BA_Converting.Between.ACSL.Annotations.and.Witness.Invariants_Umbricht.pdf}, keyword = {CPAchecker, Software Model Checking, ACSL}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  4. Benedikt Damböck. Implementierung und Evaluation von einfacher Schleifenabstraktion für das CPAchecker-Framework. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry Keyword(s): CPAchecker, Software Model Checking, Loop Acceleration
    BibTeX Entry
    @misc{DamboeckLoopAccel, author = {Benedikt Damböck}, title = {Implementierung und Evaluation von einfacher Schleifenabstraktion für das \textsc{CPAchecker}-Framework}, year = {2020}, keyword = {CPAchecker, Software Model Checking, Loop Acceleration}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  5. Sven Massard. Improve Analysis of Java Programs in CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry
    @misc{MassardJavaPrograms, author = {Sven Massard}, title = {Improve Analysis of Java Programs in \textsc{CPAchecker}}, year = {2020}, keyword = {CPAchecker, Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  6. Frederic Schönberger. Converting Test Goals to Condition Automata. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry Keyword(s): CPAchecker, Software Model Checking PDF Presentation
    BibTeX Entry
    @misc{SchoenbergerTestGoalsToConditions, author = {Frederic Sch{\"o}nberger}, title = {Converting Test Goals to Condition Automata}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Schoenberger.Converting_Test_Goals_to_Condition_Automata.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2021-01-13_BA_Converting_Test_Goals_to_Condition_Automata_Schoenberger.pdf}, keyword = {CPAchecker, Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  7. Jakob Selberg. Automatic Generation of Test Harnesses for Pointer-Based C Programs: Implementation of a Pointer-Tracking Analysis and Harness-Generation Engine in the Formal Verification Framework CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry
    @misc{SelbergHarnessesForPointers, author = {Jakob Selberg}, title = {Automatic Generation of Test Harnesses for Pointer-Based C Programs: Implementation of a Pointer-Tracking Analysis and Harness-Generation Engine in the Formal Verification Framework \textsc{CPAchecker}}, year = {2020}, keyword = {CPAchecker, Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  8. Yannick Adams. Domain Types for Predicate Analysis in CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry
    @misc{AdamsDomainTypesPredicate, author = {Yannick Adams}, title = {Domain Types for Predicate Analysis in \textsc{CPAchecker}}, year = {2020}, keyword = {CPAchecker, Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  9. Vladyslav Kolesnykov. SMT-Based Model Checking of Concurrent Programs. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry Keyword(s): CPAchecker, Software Model Checking PDF
    BibTeX Entry
    @misc{KolesnykovConcurrencySMT, author = {Vladyslav Kolesnykov}, title = {{SMT}-Based Model Checking of Concurrent Programs}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Kolesnykov.SMT-Based_Model_Checking_of_Concurrent_Programs.pdf}, keyword = {CPAchecker, Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  10. Radu-Cristian Rusanu. Interval-Based Optimization for SMT Solvers. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry Keyword(s): JavaSMT
    BibTeX Entry
    @misc{RusanuIntervalSMTSolver, author = {Radu-Cristian Rusanu}, title = {Interval-Based Optimization for SMT Solvers}, year = {2020}, keyword = {JavaSMT}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  11. Amena Abdulla. Reale Anforderungen für die Software-Analyse. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry
    BibTeX Entry
    @misc{AbdullaSARD, author = {Amena Abdulla}, title = {Reale Anforderungen f{\"u}r die Software-Analyse}, year = {2020}, keyword = {}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  12. Simon Lund. Code Complexity Measures in Software Engineering: A Systematic Comparison and Evaluation on Software-Component Level. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry PDF
    BibTeX Entry
    @misc{LundComplexityMeasures, author = {Simon Lund}, title = {Code Complexity Measures in Software Engineering: A Systematic Comparison and Evaluation on Software-Component Level}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Lund.Complexity_Measures_in_Software_Engineering.pdf}, keyword = {}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  13. Angelos Kafounis. Fault Localization in Model Checking. Implementation and Evaluation of Fault-Localization Techniques with Distance Metrics. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry Keyword(s): CPAchecker, Software Model Checking PDF Presentation
    BibTeX Entry
    @misc{KafounisFaultLocalizationWithDistanceMetrics, author = {Angelos Kafounis}, title = {Fault Localization in Model Checking. Implementation and Evaluation of Fault-Localization Techniques with Distance Metrics}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Kafounis.Fault_Localization_in_Model_Checking_Implementation_and_Evaluation_of_Fault-Localization_Techniques_with_Distance_Metrics.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2020-09-29_BA_FaultLocalizationWithDistanceMetrics_Kafounis.pdf}, keyword = {CPAchecker, Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  14. Schindar Ali. Test-Based Fault Localization in the Context of Formal Verification: Implementation and Evaluation of the Tarantula Algorithm in CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry Keyword(s): CPAchecker, Software Model Checking PDF Presentation
    BibTeX Entry
    @misc{AliFaultLocalizationWithTarantula, author = {Schindar Ali}, title = {Test-Based Fault Localization in the Context of Formal Verification: Implementation and Evaluation of the Tarantula Algorithm in CPAchecker}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Ali.Test-Based_Fault_Localization_in_the_Context_of_Formal_Verification.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2020-09-02_BA_FaultLocalizationWithTestBasedDistanceMetrics_Ali.pdf}, keyword = {CPAchecker, Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  15. Petros Isaakidis. Energy Consumption Prediction of Verification Work. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry Keyword(s): CPAchecker, Benchmarking, Energy Measurement
    BibTeX Entry
    @misc{IsaakidisEnergy, author = {Petros Isaakidis}, title = {Energy Consumption Prediction of Verification Work}, year = {2020}, keyword = {CPAchecker, Benchmarking, Energy Measurement}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  16. Matthias Kettl. Fault Localization for Formal Verification: An Implementation and Evaluation of Algorithms based on Error Invariants and UNSAT-cores. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry Keyword(s): CPAchecker, Software Model Checking PDF Presentation
    BibTeX Entry
    @misc{KettlFaultLocalization, author = {Matthias Kettl}, title = {Fault Localization for Formal Verification: An Implementation and Evaluation of Algorithms based on Error Invariants and UNSAT-cores}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Kettl.Fault_Localization_for_Formal_Verification_An_Implementation_and_Evaluation_of_Algorithms_based_on_Error_Invariants_and_UNSAT-cores.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2020-07-22_BA_FaultLocalizationWithUnsatCores_Kettl.pdf}, keyword = {CPAchecker, Software Model Checking}, annote = {Won the LMU research award for excellent students (LMU Forschungspreis f{\"u}r exzellente Studierende) of LMU Munich}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
    Additional Infos
    Won the LMU research award for excellent students (LMU Forschungspreis für exzellente Studierende) of LMU Munich
  17. Sonja Münchow. A Web Frontend For Visualization of Computation Steps and their Results in CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry Keyword(s): CPAchecker PDF Presentation
    BibTeX Entry
    @misc{MuenchowVisualizeComputationSteps, author = {Sonja M\"unchow}, title = {A Web Frontend For Visualization of Computation Steps and their Results in CPAchecker}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Muenchow.A_Web_Frontend_for_Visualization_of_Computation_Steps_and_their_Results_in_CPAchecker.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2020-07-15_BA_WebFrontendForVisualizationOfComputationStepsInCpachecker_Muenchow.pdf}, keyword = {CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  18. Adrian Leimeister. A Language Server and IDE Plugin for CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry Keyword(s): CPAchecker PDF Presentation
    BibTeX Entry
    @misc{LeimeisterIdeLsp, author = {Adrian Leimeister}, title = {A Language Server and IDE Plugin for \textsc{CPAchecker}}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Leimeister.A_Language_Server_and_IDE_Plugin_for_CPAchecker.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2020-07-15_BA_IdePluginForCpachecker_Leimeister.pdf}, keyword = {CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  19. Michael Obermeier. Extending the Framework JavaSMT with the SMT Solver Yices2. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry Keyword(s): JavaSMT PDF Presentation
    BibTeX Entry
    @misc{ObermeierYices2, author = {Michael Obermeier}, title = {Extending the Framework {{\sc JavaSMT}} with the {SMT} Solver {{\sc Yices2}}}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Obermeier.Extending_the_Framework_JavaSMT_with_the_SMT_Solver_Yices2.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2020-05-13_BA_IntegrationYices2InJavaSMT_Obermeier.pdf}, keyword = {JavaSMT}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  20. Alexander Ried. Design and Implementation of a Cluster-Based Approach for Software Verification. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry Keyword(s): CPAchecker, BAM
    BibTeX Entry
    @misc{RiedClusterBAM, author = {Alexander Ried}, title = {Design and Implementation of a Cluster-Based Approach for Software Verification}, year = {2020}, keyword = {CPAchecker, BAM}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  21. Tillmann Gaida. SMT-based Checking and Synthesis of Formal Refinements. Master's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry
    BibTeX Entry
    @misc{GaidaRefinement, author = {Tillmann Gaida}, title = {SMT-based Checking and Synthesis of Formal Refinements}, year = {2020}, field = {Computer Science}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
  22. Lukas Rieger. Information Flow Testing of a PGP Server. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry
    BibTeX Entry
    @misc{RiegerPGP, author = {Lukas Rieger}, title = {Information Flow Testing of a PGP Server}, year = {2020}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  23. Hyunsung Kim. Coverage-guided Fuzzing with Stochastic Optimization. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020. Link to this entry
    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}, }

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: Mon Nov 18 19:35:54 2024 UTC