3 Papers accepted at ISoLA'20: "An Interface Theory for Program Verification", "Verification Artifacts in Cooperative Verification", and "Violation Witnesses and Result Validation for Multi-Threaded Programs"

Publications of year 2020

(All PublicationsIndex)

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.
    [ Material ] [ Article ]
    @Proceedings{VMCAI20,
    editor = {Dirk Beyer and Damien Zufferey},
    title = {Proceedings of the 21st International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)},
    publisher = {Springer},
    series = {LNCS~11990},
    year = {2020},
    isbn = {978-3-030-39321-2},
    doi = {10.1007/978-3-030-39322-9},
    pdf = {https://doi.org/10.1007/978-3-030-39322-9},
    url = {https://popl20.sigplan.org/home/VMCAI-2020},
    
    }
    

Articles in journal or book chapters

  1. Thomas Lemberger.
    Plain random test generation with PRTest.
    International Journal on Software Tools for Technology Transfer (STTT), 2020.
    [ Article ] [ Presentation ] Keyword(s): Software Testing.
    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.
    DOI: https://doi.org/10.1007/s10009-020-00568-x
    Publication appeared first online in July 2020.
    PRTest is available at: https://gitlab.com/sosy-lab/software/prtest

    @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},
    pdf = {https://www.sosy-lab.org/research/pub/2020-STTT.Plain_random_test_generation_with_PRTest.pdf},
    postscript= {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 = {DOI: https://doi.org/10.1007/s10009-020-00568-x
    Publication appeared first online in July 2020.
    PRTest is available at: https://gitlab.com/sosy-lab/software/prtest}, }

Articles in conference or workshop proceedings

  1. 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.
    [ Material ] [ Article ] Keyword(s): Competition on Software Verification (SV-COMP), Competition on Software Verification (SV-COMP Report), Software Model Checking.
    Abstract


    @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},
    series = {LNCS~12079},
    publisher = {Springer},
    pages = {347-367},
    year = {2020},
    doi = {10.1007/978-3-030-45237-7_21},
    pdf = {https://doi.org/10.1007/978-3-030-45237-7_21},
    url = {https://sv-comp.sosy-lab.org/},
    keyword = {Competition on Software Verification (SV-COMP),Competition on Software Verification (SV-COMP Report),Software Model Checking},
    abstract = { },
    
    }
    

  2. Dirk Beyer.
    Second Competition on Software Testing: Test-Comp 2020.
    In Proceedings of the 22nd International Conference on Fundamental Approaches to Software Engineering (FASE 2020, Dublin, Ireland, April 25-30), LNCS 12076, pages 505-519, 2020.
    Springer.
    [ Material ] [ Article ] Keyword(s): Competition on Software Testing (Test-Comp), Competition on Software Testing (Test-Comp Report), Software Testing.
    Abstract


    @InProceedings{FASE20,
    author = {Dirk Beyer},
    title = {Second Competition on Software Testing: Test-Comp 2020},
    booktitle = {Proceedings of the 22nd International Conference on Fundamental Approaches to Software Engineering (FASE~2020, Dublin, Ireland, April 25-30)},
    series = {LNCS~12076},
    publisher = {Springer},
    pages = {505-519},
    year = {2020},
    doi = {10.1007/978-3-030-45234-6_25},
    pdf = {https://doi.org/10.1007/978-3-030-45234-6_25},
    url = {https://test-comp.sosy-lab.org/},
    keyword = {Competition on Software Testing (Test-Comp),Competition on Software Testing (Test-Comp Report),Software Testing},
    abstract = { },
    
    }
    

  3. 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.
    [ Material ] [ Article ] Keyword(s): Software Model Checking.
    Abstract


    @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},
    series = {LNCS~12078},
    publisher = {Springer},
    pages = {3-21},
    year = {2020},
    doi = {10.1007/978-3-030-45190-5_1},
    pdf = {https://doi.org/10.1007/978-3-030-45190-5_1},
    url = {https://www.sosy-lab.org/research/pdr-compare/},
    keyword = {Software Model Checking},
    abstract = { },
    
    }
    

  4. 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, Part 1, Rhodos, Greece, October 26-30), LNCS, 2020.
    Springer.
    [ Material ] [ Article ] Keyword(s): DFG-CONVEY, CPAchecker, Software Model Checking, Witness-Based Validation, Witness-Based Validation (main).
    Abstract


    @inproceedings{ISoLA20a,
    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, Part~1, Rhodos, Greece, October 26-30)},
    editor = {T.~Margaria and B.~Steffen},
    publisher = {Springer},
    series = {LNCS~},
    pages = {},
    year = {2020},
    doi = {},
    pdf = {https://www.sosy-lab.org/research/pub/2020-ISOLA.Violation_Witnesses_and_Result_Validation_for_Multi-Threaded_Programs.pdf},
    postscript= {},
    url = {https://www.sosy-lab.org/research/witnesses-concurrency/},
    keyword = {DFG-CONVEY,CPAchecker,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)},
    abstract = { 
    
    },
    
    }
    

  5. 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.
    Abstract


    @inproceedings{SE20,
    author = {Dirk Beyer and Marie-Christine Jakobs},
    editor = {M.~Felderer and W.~Hasselbring and R.~Rabiser and R.~Jung},
    title = {Cooperative Test-Case Generation with Verifiers},
    booktitle = {Proceedings of the Conference on Software Engineering (SE~2020, Innsbruck, Austria, February 24-28)},
    series = {{LNI}~P-300},
    pages = {107--108},
    publisher = {{GI}},
    year = {2020},
    doi = {10.18420/SE2020\_31},
    isbnnote = {978-3-88579-694-7},
    pdf = {},
    postscript = {},
    abstract = { },
    
    }
    

  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.
    [ Material ] [ Article ] Keyword(s): DFG-COOP, CPAchecker, Software Model Checking.
    Abstract


    @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},
    series = {LNCS~12310},
    pages = {113--132},
    year = {2020},
    publisher = {Springer},
    doi = {10.1007/978-3-030-58768-0_7},
    pdf = {https://www.sosy-lab.org/research/pub/2020-SEFM.FRed_Conditional_Model_Checking_via_Reducers_and_Folders.pdf},
    url = {https://www.sosy-lab.org/research/fred/},
    isbnnote = {},
    keyword = {DFG-COOP,CPAchecker,Software Model Checking},
    abstract = { },
    
    }
    

  7. 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.
    [ Material ] [ Article ] [ Presentation ] Keyword(s): DFG-CONVEY, DFG-COOP, CPAchecker, Software Model Checking.
    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.

    @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},
    series = {LNCS~12310},
    pages = {133--154},
    year = {2020},
    publisher = {Springer},
    doi = {10.1007/978-3-030-58768-0_8},
    pdf = {https://www.sosy-lab.org/research/pub/2020-SEFM.Difference_Verification_with_Conditions.pdf},
    url = {https://www.sosy-lab.org/research/difference/},
    postscript = {https://www.sosy-lab.org/research/prs/2020-09-17_SEFM20_DifferenceVerificationWithConditions_Thomas.pdf},
    isbnnote = {},
    keyword = {DFG-CONVEY,DFG-COOP,CPAchecker,Software Model Checking},
    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. },
    
    }
    

  8. 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, Part 1, Rhodos, Greece, October 26-30), LNCS, 2020.
    Springer.
    [ Article ] Keyword(s): DFG-CONVEY, CPAchecker, Software Model Checking, Interfaces for Component-Based Design.
    Abstract


    @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, Part~1, Rhodos, Greece, October 26-30)},
    editor = {T.~Margaria and B.~Steffen},
    publisher = {Springer},
    series = {LNCS~},
    pages = {},
    year = {2020},
    doi = {},
    pdf = {https://www.sosy-lab.org/research/pub/2020-ISOLA.An_Interface_Theory_for_Program_Verification.pdf},
    postscript= {},
    url = {},
    keyword = {DFG-CONVEY,CPAchecker,Software Model Checking,Interfaces for Component-Based Design},
    abstract = { 
    
    },
    
    }
    

  9. 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.
    [ Material ] [ Article ] Keyword(s): DFG-CONVEY, CPAchecker, Software Model Checking, Witness-Based Validation, Witness-Based Validation (main).
    Abstract


    @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},
    series = {LNCS~12225},
    publisher = {Springer},
    pages = {165-177},
    year = {2020},
    doi = {10.1007/978-3-030-53291-8_10},
    pdf = {https://www.sosy-lab.org/research/pub/2020-CAV.MetaVal_Witness_Validation_via_Verification.pdf},
    url = {https://gitlab.com/sosy-lab/software/metaval},
    isbnnote = {978-3-030-53290-1},
    keyword = {DFG-CONVEY,CPAchecker,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)},
    abstract = { },
    
    }
    

  10. 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, Part 1, Rhodos, Greece, October 26-30), LNCS, 2020.
    Springer.
    [ Article ] Keyword(s): DFG-COOP, CPAchecker, Software Model Checking.
    Abstract


    @inproceedings{ISoLA20c,
    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, Part~1, Rhodos, Greece, October 26-30)},
    editor = {T.~Margaria and B.~Steffen},
    publisher = {Springer},
    series = {LNCS~},
    pages = {},
    year = {2020},
    doi = {},
    pdf = {https://www.sosy-lab.org/research/pub/2020-ISOLA.Verification_Artifacts_in_Cooperative_Verification_Survey_and_Unifying_Component_Framework.pdf},
    postscript= {},
    url = {},
    keyword = {DFG-COOP,CPAchecker,Software Model Checking},
    abstract = { 
    
    },
    
    }
    

  11. 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.
    [ Material ] [ Article ] Keyword(s): Benchmarking.
    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.

    @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},
    series = {LNCS~12079},
    publisher = {Springer},
    pages = {126-133},
    year = {2020},
    doi = {10.1007/978-3-030-45237-7_8},
    pdf = {https://doi.org/10.1007/978-3-030-45237-7_8},
    url = {https://www.sosy-lab.org/research/energy-measurement/},
    keyword = {Benchmarking},
    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. },
    
    }
    

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

  1. 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.
    [ Article ] [ Presentation ] Keyword(s): CPAchecker, Software Model Checking.

    @misc{AliFaultLocalizationWithTarantula,
    pdf = {https://www.sosy-lab.org/research/bsc/2020.Ali.Test-based_Fault_Localization_in_the_Context_of_Formal_Verification.pdf},
    postscript = {https://www.sosy-lab.org/research/prs/2020-09-02_BA_FaultLocalizationWithTestBasedDistanceMetrics_Ali.pdf},
    author = {Schindar Ali},
    title = {Test-based Fault Localization in the Context of Formal Verification: Implementation and Evaluation of the Tarantula Algorithm in CPAchecker},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2020},
    field = {Computer Science},
    keyword = {CPAchecker, Software Model Checking},
    
    }
    

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

    @misc{BeckSeparationLogic,
    author = {Moritz Beck},
    title = {Solver-based Analysis of Memory Safety using Separation Logic},
    howpublished = {Master's Thesis, LMU Munich, Software Systems Lab},
    year = {2020},
    pdf = {https://www.sosy-lab.org/research/msc/2020.Beck.Solver-based_Analysis_of_Memory_Safety_using_Separation_Logic.pdf},
    postscript = {https://www.sosy-lab.org/research/prs/2020-09-16_MA_SolverBasedAnalysisOfMemorySafetyUsingSeparationLogic_Beck.pdf},
    keyword = {CPAchecker,JavaSMT,Separation Logic,Software Model Checking},
    
    }
    

  3. Petros Isaakidis.
    Energy Consumption Prediction of Verification Work.
    Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020.
    Keyword(s): CPAchecker, Benchmarking, Energy Measurement.

    @misc{IsaakidisEnergy,
    %Permission not yet requested % pdf = {https://www.sosy-lab.org/research/bsc/2020.Isaakidis.Energy_Consumption_Prediction_of_Verification_Work.pdf},
    % postscript = {},
    author = {Petros Isaakidis},
    title = {Energy Consumption Prediction of Verification Work},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2020},
    field = {Computer Science},
    keyword = {CPAchecker, Benchmarking, Energy Measurement},
    
    }
    

  4. 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.
    [ Article ] Keyword(s): CPAchecker, Software Model Checking.

    @misc{KafounisFaultLocalizationWithDistanceMetrics,
    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},
    %postscript = {},
    author = {Angelos Kafounis},
    title = {Fault Localization in Model Checking. Implementation and Evaluation of Fault-Localization Techniques with Distance Metrics},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2020},
    field = {Computer Science},
    keyword = {CPAchecker, Software Model Checking},
    
    }
    

  5. 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.
    [ Article ] [ Presentation ] Keyword(s): CPAchecker, Software Model Checking.

    @misc{KettlFaultLocalization,
    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},
    postscript = {https://www.sosy-lab.org/research/prs/2020-07-22_BA_FaultLocalizationWithUnsatCores_Kettl.pdf},
    author = {Matthias Kettl},
    title = {Fault Localization for Formal Verification. An Implementation and Evaluation of Algorithms based on Error Invariants and UNSAT-cores},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2020},
    field = {Computer Science},
    keyword = {CPAchecker, Software Model Checking},
    
    }
    

  6. Adrian Leimeister.
    A Language Server and IDE Plugin for CPAchecker.
    Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020.
    [ Article ] [ Presentation ] Keyword(s): CPAchecker.

    @misc{LeimeisterIdeLsp,
    pdf = {https://www.sosy-lab.org/research/bsc/2020.Leimeister.A_Language_Server_and_IDE_Plugin_for_CPAchecker.pdf},
    postscript = {https://www.sosy-lab.org/research/prs/2020-07-15_BA_IdePluginForCpachecker_Leimeister.pdf},
    author = {Adrian Leimeister},
    title = {A Language Server and IDE Plugin for CPAchecker},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2020},
    field = {Computer Science},
    keyword = {CPAchecker},
    
    }
    

  7. 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.
    [ Article ] [ Presentation ] Keyword(s): CPAchecker.

    @misc{MuenchowVisualizeComputationSteps,
    pdf = {https://www.sosy-lab.org/research/bsc/2020.Muenchow.A_Web_Frontend_for_Visualization_of_Computation_Steps_and_their_Results_in_CPAchecker.pdf},
    postscript = {https://www.sosy-lab.org/research/prs/2020-07-15_BA_WebFrontendForVisualizationOfComputationStepsInCpachecker_Muenchow.pdf},
    author = {Sonja M\"unchow},
    title = {A Web Frontend For Visualization of Computation Steps and their Results in CPAchecker},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2020},
    field = {Computer Science},
    keyword = {CPAchecker},
    
    }
    

  8. Michael Obermeier.
    Extending the Framework JavaSMT with the SMT Solver Yices2.
    Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020.
    [ Article ] [ Presentation ] Keyword(s): JavaSMT.

    @misc{ObermeierYices2,
    pdf = {https://www.sosy-lab.org/research/bsc/2020.Obermeier.Extending_the_Framework_JavaSMT_with_the_SMT_Solver_Yices2.pdf},
    postscript = {https://www.sosy-lab.org/research/prs/2020-05-13_BA_IntegrationYices2InJavaSMT_Obermeier.pdf},
    author = {Michael Obermeier},
    title = {Extending the Framework {{\sc JavaSMT}} with the {SMT} Solver {{\sc Yices2}}},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2020},
    field = {Computer Science},
    keyword = {JavaSMT},
    
    }
    

  9. Alexander Ried.
    Design and Implementation of a Cluster-Based Approach for Software Verification.
    Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020.
    Keyword(s): CPAchecker, BAM.

    @misc{RiedClusterBAM,
    author = {Alexander Ried},
    title = {Design and Implementation of a Cluster-Based Approach for Software Verification},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2020},
    field = {Computer Science},
    keyword = {CPAchecker, BAM},
    
    }
    

(All PublicationsIndex)



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: Sun Sep 27 12:34:20 2020


This document was translated from BibTEX by bibtex2html