We are hiring new doctoral researchers, student research assistants, and tutors. Apply now!
We receive 5 Contributor Projects for Google Summer of Code 2024

Publications of year 2023

Articles in journal or book chapters

  1. Manfred Broy, Albrecht Schmidt, and Martin Wirsing. In memory of Heinrich Hussmann, long-time friend and SoSyM editor. Softw. Syst. Model., 22(2):453-454, 2023. doi:10.1007/s10270-023-01099-0 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @article{NachrufHussmann, author = {Manfred Broy and Albrecht Schmidt and Martin Wirsing}, title = {In memory of Heinrich Hussmann, long-time friend and SoSyM editor}, journal = {Softw. Syst. Model.}, volume = {22}, number = {2}, pages = {453--454}, year = {2023}, doi = {10.1007/s10270-023-01099-0}, pdf = {https://sosy-lab.org/research/pub/2023-SoSyM.In_memory_of_Heinrich_Hussmann_long-time_friend_and_SoSyM_editor.pdf}, }

Articles in conference or workshop proceedings

  1. Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. CPA-DF: A Tool for Configurable Interval Analysis to Boost Program Verification. In Proc. ASE, pages 2050-2053, 2023. IEEE. doi:10.1109/ASE56229.2023.00213 Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, CPAchecker Funding: DFG-CONVEY Publisher's Version PDF Presentation Video Supplement
    Artifact(s)
    Abstract
    Software verification is challenging, and auxiliary program invariants are used to improve the effectiveness of verification approaches. For instance, the k-induction implementation in CPAchecker, an award-winning framework for program analysis, uses invariants produced by a configurable data-flow analysis to strengthen induction hypotheses. This invariant generator, CPA-DF, uses arithmetic expressions over intervals as its abstract domain and is able to prove some safe verification tasks alone. After extensively evaluating CPA-DF on SV-Benchmarks, the largest publicly available suite of C safety-verification tasks, we discover that its potential as a stand-alone analysis or a sub-analysis in a parallel portfolio for combined verification approaches has been significantly underestimated: (1) As a stand-alone analysis, CPA-DF finds almost as many proofs as the plain k-induction implementation without auxiliary invariants. (2) As a sub-analysis running in parallel to the plain k-induction implementation, CPA-DF boosts the portfolio verifier to solve a comparable amount of tasks as the heavily-optimized k-induction implementation with invariant injection. Our detailed analysis reveals that dynamic precision adjustment is crucial to the efficiency and effectiveness of CPA-DF. To generalize our results beyond CPAchecker, we use CoVeriTeam, a platform for cooperative verification, to compose three portfolio verifiers that execute CPA-DF and three other software verifiers in parallel, respectively. Surprisingly, running CPA-DF merely in parallel to these state-of-the-art tools further boosts the number of correct results up to more than 20%.
    Demonstration video: https://youtu.be/l7UG-vhTL_4
    BibTeX Entry
    @inproceedings{ASE23a, author = {Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {{CPA-DF}: {A} Tool for Configurable Interval Analysis to Boost Program Verification}, booktitle = {Proc.\ ASE}, pages = {2050-2053}, year = {2023}, series = {}, publisher = {IEEE}, doi = {10.1109/ASE56229.2023.00213}, url = {https://www.sosy-lab.org/research/cpa-df/}, pdf = {https://www.sosy-lab.org/research/pub/2023-ASE.CPA-DF_A_Tool_for_Configurable_Interval_Analysis_to_Boost_Program_Verification.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2023-09-13_ASE_CPA-DF_Po-Chun.pdf}, abstract = {Software verification is challenging, and auxiliary program invariants are used to improve the effectiveness of verification approaches. For instance, the <i>k</i>-induction implementation in <a href="https://cpachecker.sosy-lab.org/">CPAchecker</a>, an award-winning framework for program analysis, uses invariants produced by a configurable data-flow analysis to strengthen induction hypotheses. This invariant generator, CPA-DF, uses arithmetic expressions over intervals as its abstract domain and is able to prove some safe verification tasks alone. After extensively evaluating CPA-DF on <a href="https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks">SV-Benchmarks</a>, the largest publicly available suite of C safety-verification tasks, we discover that its potential as a stand-alone analysis or a sub-analysis in a parallel portfolio for combined verification approaches has been significantly underestimated: (1) As a stand-alone analysis, CPA-DF finds almost as many proofs as the plain <i>k</i>-induction implementation without auxiliary invariants. (2) As a sub-analysis running in parallel to the plain <i>k</i>-induction implementation, CPA-DF boosts the portfolio verifier to solve a comparable amount of tasks as the heavily-optimized <i>k</i>-induction implementation with invariant injection. Our detailed analysis reveals that dynamic precision adjustment is crucial to the efficiency and effectiveness of CPA-DF. To generalize our results beyond CPAchecker, we use <a href="https://gitlab.com/sosy-lab/software/coveriteam">CoVeriTeam</a>, a platform for cooperative verification, to compose three portfolio verifiers that execute CPA-DF and three other software verifiers in parallel, respectively. Surprisingly, running CPA-DF merely in parallel to these state-of-the-art tools further boosts the number of correct results up to more than 20&percnt;. <br> Demonstration video: <a href="https://youtu.be/l7UG-vhTL_4">https://youtu.be/l7UG-vhTL_4</a>}, keyword = {Software Model Checking, Cooperative Verification, CPAchecker}, artifact = {10.5281/zenodo.8245821}, funding = {DFG-CONVEY}, video = {https://youtu.be/l7UG-vhTL_4}, }
  2. Dirk Beyer and Martin Spiessl. LIV: Invariant Validation using Straight-Line Programs. In Proc. ASE, pages 2074-2077, 2023. IEEE. doi:10.1109/ASE56229.2023.00214 Link to this entry Keyword(s): Software Model Checking, Witness-Based Validation Funding: DFG-CONVEY Publisher's Version PDF Video Supplement
    Artifact(s)
    Abstract
    Validation of correctness proofs is an established procedure in software verification. While there are steady advances when it comes to verification of more and more complex software systems, it becomes increasingly hard to determine which information is actually useful for validation of the correctness proof. Usually, the central piece that verifiers struggle to come up with are good loop invariants. While a proof using inductive invariants is easy to validate, not all invariants used by verifiers necessarily are inductive. In order to alleviate this problem, we propose LIV, an approach that makes it easy to check if the invariant information provided by the verifier is sufficient to establish an inductive proof. This is done by emulating a Hoare-style proof, splitting the program into Hoare triples and converting these into verification tasks that can themselves be efficiently verified by an off-the-shelf verifier. In case the validation fails, useful information about the failure reason can be extracted from the overview of which triples could be established and which were refuted. We show that our approach works by evaluating it on a state-of-the-art benchmark set.
    BibTeX Entry
    @inproceedings{ASE23b, author = {Dirk Beyer and Martin Spiessl}, title = {LIV: Invariant Validation using Straight-Line Programs}, booktitle = {Proc.\ ASE}, pages = {2074-2077}, year = {2023}, series = {}, publisher = {IEEE}, doi = {10.1109/ASE56229.2023.00214}, url = {https://www.sosy-lab.org/research/liv}, pdf = {https://www.sosy-lab.org/research/pub/2023-ASE.LIV_Loop-Invariant_Validation_using_Straight-Line_Programs.pdf}, abstract = {Validation of correctness proofs is an established procedure in software verification. While there are steady advances when it comes to verification of more and more complex software systems, it becomes increasingly hard to determine which information is actually useful for validation of the correctness proof. Usually, the central piece that verifiers struggle to come up with are good loop invariants. While a proof using inductive invariants is easy to validate, not all invariants used by verifiers necessarily are inductive. In order to alleviate this problem, we propose LIV, an approach that makes it easy to check if the invariant information provided by the verifier is sufficient to establish an inductive proof. This is done by emulating a Hoare-style proof, splitting the program into Hoare triples and converting these into verification tasks that can themselves be efficiently verified by an off-the-shelf verifier. In case the validation fails, useful information about the failure reason can be extracted from the overview of which triples could be established and which were refuted. We show that our approach works by evaluating it on a state-of-the-art benchmark set.}, keyword = {Software Model Checking, Witness-Based Validation}, artifact = {10.5281/zenodo.8289101}, funding = {DFG-CONVEY}, video = {https://youtu.be/mZhoGAa08Rk}, }
  3. Dirk Beyer, Marian Lingsch-Rosenfeld, and Martin Spiessl. CEGAR-PT: A Tool for Abstraction by Program Transformation. In Proc. ASE, pages 2078-2081, 2023. IEEE. doi:10.1109/ASE56229.2023.00215 Link to this entry Keyword(s): Software Model Checking Funding: DFG-CONVEY Publisher's Version PDF Video Supplement
    Artifact(s)
    Abstract
    Abstraction is a key technology for proving the correctness of computer programs. There are many approaches available, but unfortunately, the various techniques are difficult to combine and the successful techniques have to be re-implemented again and again.
    We address this problem by using the tool CEGAR-PT, which views abstraction as program transformation and integrates different verification components off-the-shelf. The idea is to use existing components without having to change their implementation, while still adjusting the precision of the abstraction using the successful CEGAR approach. The approach is largely general: it only restricts the abstraction to transform, given a precision that defines the level of abstraction, one program into another program. The abstraction by program transformation can over-approximate the data flow (e.g., havoc some variables, use more abstract types) or the control flow (e.g., loop abstraction, slicing).
    BibTeX Entry
    @inproceedings{ASE23c, author = {Dirk Beyer and Marian Lingsch-Rosenfeld and Martin Spiessl}, title = {CEGAR-PT: A Tool for Abstraction by Program Transformation}, booktitle = {Proc.\ ASE}, pages = {2078-2081}, year = {2023}, series = {}, publisher = {IEEE}, doi = {10.1109/ASE56229.2023.00215}, url = {https://www.sosy-lab.org/research/cegar-pt}, pdf = {https://www.sosy-lab.org/research/pub/2023-ASE.CEGAR-PT_A_Tool_for_Abstraction_by_Program_Transformation.pdf}, abstract = {Abstraction is a key technology for proving the correctness of computer programs. There are many approaches available, but unfortunately, the various techniques are difficult to combine and the successful techniques have to be re-implemented again and again. <br> We address this problem by using the tool CEGAR-PT, which views abstraction as program transformation and integrates different verification components off-the-shelf. The idea is to use existing components without having to change their implementation, while still adjusting the precision of the abstraction using the successful CEGAR approach. The approach is largely general: it only restricts the abstraction to transform, given a precision that defines the level of abstraction, one program into another program. The abstraction by program transformation can over-approximate the data flow (e.g., havoc some variables, use more abstract types) or the control flow (e.g., loop abstraction, slicing).}, keyword = {Software Model Checking}, artifact = {10.5281/zenodo.8287183}, funding = {DFG-CONVEY}, video = {https://youtu.be/ASZ6hoq8asE}, }
  4. Dirk Beyer, Sudeep Kanav, and Henrik Wachowitz. CoVeriTeam Service: Verification as a Service. In Proc. ICSE, pages 21-25, 2023. IEEE. doi:10.1109/ICSE-Companion58688.2023.00017 Link to this entry Keyword(s): Software Model Checking, Incremental Verification, Cooperative Verification Funding: DFG-CONVEY, DFG-COOP Publisher's Version PDF Supplement
    Artifact(s)
    Abstract
    The research community has developed numerous tools for solving verification problems, but we are missing a common interface for executing them. This means users have to spend considerable effort on the installation and parameter setup, for each new tool (version) they want to execute. The situation could make a verification researcher wanting to experiment with a new verification tool turn away from it. We aim to make it easier for users to execute verification tools, as well as provide mechanism for tool developers to make their tools easily accessible. Our solution combines a web service and a common interface for verification tools. The presented service has been used during the 2023 competitions on software verification and testing, for integration testing. As another use- case, we developed a service for incremental verification on top of the CoVeriTeam Service and demonstrate its use in a continuous-integration process.
    BibTeX Entry
    @inproceedings{ICSE23, author = {Dirk Beyer and Sudeep Kanav and Henrik Wachowitz}, title = {{CoVeriTeam} Service: Verification as a Service}, booktitle = {Proc.\ ICSE}, pages = {21-25}, year = {2023}, publisher = {IEEE}, doi = {10.1109/ICSE-Companion58688.2023.00017}, url = {https://coveriteam-service.sosy-lab.org/static/index.html}, pdf = {https://www.sosy-lab.org/research/pub/2023-ICSE.CoVeriTeam_Service_Verification_as_a_Service.pdf}, abstract = {The research community has developed numerous tools for solving verification problems, but we are missing a common interface for executing them. This means users have to spend considerable effort on the installation and parameter setup, for each new tool (version) they want to execute. The situation could make a verification researcher wanting to experiment with a new verification tool turn away from it. We aim to make it easier for users to execute verification tools, as well as provide mechanism for tool developers to make their tools easily accessible. Our solution combines a web service and a common interface for verification tools. The presented service has been used during the 2023 competitions on software verification and testing, for integration testing. As another use- case, we developed a service for incremental verification on top of the {CoVeriTeam} Service and demonstrate its use in a continuous-integration process.}, keyword = {Software Model Checking,Incremental Verification,Cooperative Verification}, _sha256 = {604dd391b6a49e46e97b6faafbb3cc331ccf5c04e3d364cf1e76a2c99c1c267f}, artifact = {10.5281/zenodo.7276532}, funding = {DFG-CONVEY,DFG-COOP}, }
  5. Dirk Beyer. Software Testing: 5th Comparative Evaluation: Test-Comp 2023. In L. Lambers and S. Uchitel, editors, Proceedings of the 26th International Conference on Fundamental Approaches to Software Engineering (FASE 2023, Paris, France, April 22-27), LNCS 13991, pages 309-323, 2023. Springer. doi:10.1007/978-3-031-30826-0_17 Link to this entry Keyword(s): Competition on Software Testing (Test-Comp), Competition on Software Testing (Test-Comp Report), Software Testing Funding: DFG-COOP Publisher's Version PDF Supplement
    BibTeX Entry
    @inproceedings{FASE23, author = {Dirk Beyer}, title = {Software Testing: 5th Comparative Evaluation: {Test-Comp 2023}}, booktitle = {Proceedings of the 26th International Conference on Fundamental Approaches to Software Engineering (FASE~2023, Paris, France, April 22-27)}, editor = {L. Lambers and S. Uchitel}, pages = {309--323}, year = {2023}, series = {LNCS~13991}, publisher = {Springer}, isbn = {}, doi = {10.1007/978-3-031-30826-0_17}, sha256 = {7110c26bf3c9311f84346a108a59318687bdadde4879f83d047f1a0fc546b630}, url = {https://test-comp.sosy-lab.org/2023/}, keyword = {Competition on Software Testing (Test-Comp),Competition on Software Testing (Test-Comp Report),Software Testing}, _pdf = {https://www.sosy-lab.org/research/pub/2023-FASE.Software_Testing_5th_Comparative_Evaluation_Test-Comp_2023.pdf}, funding = {DFG-COOP}, }
  6. Dirk Beyer. Competition on Software Verification and Witness Validation: SV-COMP 2023. In S. Sankaranarayanan and N. Sharygina, editors, Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023, Paris, France, April 22-27), LNCS 13994, pages 495-522, 2023. Springer. doi:10.1007/978-3-031-30820-8_29 Link to this entry Keyword(s): Competition on Software Verification (SV-COMP), Competition on Software Verification (SV-COMP Report), Software Model Checking Funding: DFG-COOP Publisher's Version PDF Supplement
    BibTeX Entry
    @inproceedings{TACAS23b, author = {Dirk Beyer}, title = {Competition on Software Verification and Witness Validation: {SV-COMP 2023}}, booktitle = {Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2023, Paris, France, April 22-27)}, editor = {S. Sankaranarayanan and N. Sharygina}, pages = {495--522}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_29}, sha256 = {1d35ae38d4e87c267ccc34cba880994b6f6a7927491ec13ba3cc548a29e81e5c}, url = {https://sv-comp.sosy-lab.org/2023/}, keyword = {Competition on Software Verification (SV-COMP),Competition on Software Verification (SV-COMP Report),Software Model Checking}, _pdf = {https://www.sosy-lab.org/research/pub/2023-TACAS.Competition_on_Software_Verification_and_Witness_Validation_SV-COMP_2023.pdf}, funding = {DFG-COOP}, }
  7. Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Translator. In Proc. TACAS, LNCS 13994, pages 152-172, 2023. Springer. doi:10.1007/978-3-031-30820-8_12 Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, Btor2 Funding: DFG-CONVEY Publisher's Version PDF Presentation Supplement
    Artifact(s)
    Abstract
    Across the broad field for the analysis of computational systems, research endeavors are often categorized by the respective models under investigation. Algorithms and tools are usually developed for a specific model, hindering their applications to similar problems originating from other computational systems. A prominent example of such situation is the studies on formal verification and testing for hardware and software systems. The two research communities share common theoretical foundations and solving methods, including satisfiability, interpolation, and abstraction refinement. Nevertheless, it is often demanding for one community to benefit from the advancements of the other, as analyzers typically assume a particular input format. To bridge the gap between the hardware and software analysis, we propose Btor2C, a converter from word-level sequential circuits to C programs. We choose the Btor2 language as the input format for its simplicity and bit-precise semantics. It can be deemed as an intermediate representation tailored for analysis. Given a Btor2 circuit, Btor2C generates a behaviorally equivalent program in the C language, supported by most static program analyzers. We demonstrate the use cases of Btor2C by translating the benchmark set from the Hardware Model Checking Competitions into C programs and analyze them by tools from the Competitions on Software Verification and Testing. Our results show that software analyzers can complement hardware verifiers for enhanced quality assurance.
    BibTeX Entry
    @inproceedings{TACAS23a, author = {Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {Bridging Hardware and Software Analysis with {Btor2C}: {A} Word-Level-Circuit-to-{C} Translator}, booktitle = {Proc.\ TACAS}, pages = {152-172}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_12}, url = {https://www.sosy-lab.org/research/btor2c/}, presentation = {https://www.sosy-lab.org/research/prs/2023-04-26_TACAS23_Bridging_Hardware_and_Software_Analysis_with_Btor2C_Po-Chun.pdf}, abstract = {Across the broad field for the analysis of computational systems, research endeavors are often categorized by the respective models under investigation. Algorithms and tools are usually developed for a specific model, hindering their applications to similar problems originating from other computational systems. A prominent example of such situation is the studies on formal verification and testing for hardware and software systems. The two research communities share common theoretical foundations and solving methods, including satisfiability, interpolation, and abstraction refinement. Nevertheless, it is often demanding for one community to benefit from the advancements of the other, as analyzers typically assume a particular input format. To bridge the gap between the hardware and software analysis, we propose Btor2C, a converter from word-level sequential circuits to C programs. We choose <a href="https://doi.org/10.1007/978-3-319-96145-3_32">the Btor2 language</a> as the input format for its simplicity and bit-precise semantics. It can be deemed as an intermediate representation tailored for analysis. Given a Btor2 circuit, Btor2C generates a behaviorally equivalent program in the C language, supported by most static program analyzers. We demonstrate the use cases of Btor2C by translating the benchmark set from the Hardware Model Checking Competitions into C programs and analyze them by tools from the Competitions on Software Verification and Testing. Our results show that software analyzers can complement hardware verifiers for enhanced quality assurance.}, keyword = {Software Model Checking, Cooperative Verification, Btor2}, _pdf = {https://www.sosy-lab.org/research/pub/2023-TACAS.Bridging_Hardware_and_Software_Analysis_with_Btor2C_A_Word-Level-Circuit-to-C_Translator.pdf}, artifact = {10.5281/zenodo.7551707}, funding = {DFG-CONVEY}, }
  8. Dirk Beyer, Jan Haltermann, Thomas Lemberger, and Heike Wehrheim. Component-based CEGAR - Building Software Verifiers from Off-the-Shelf Components. In G. Engels, R. Hebig, and M. Tichy, editors, Software Engineering 2023, Fachtagung des GI-Fachbereichs Softwaretechnik, 20.-24. Februar 2023, Paderborn, LNI P-332, pages 37-38, 2023. GI. Link to this entry Keyword(s): CPAchecker, Software Model Checking, Cooperative Verification Publisher's Version PDF
    BibTeX Entry
    @inproceedings{SE23, author = {Dirk Beyer and Jan Haltermann and Thomas Lemberger and Heike Wehrheim}, title = {Component-based {CEGAR} - Building Software Verifiers from Off-the-Shelf Components}, booktitle = {Software Engineering 2023, Fachtagung des GI-Fachbereichs Softwaretechnik, 20.-24. Februar 2023, Paderborn}, editor = {G.~Engels and R.~Hebig and M.~Tichy}, pages = {37--38}, year = {2023}, series = {{LNI}~P-332}, publisher = {{GI}}, sha256 = {}, pdf = {https://sosy-lab.org/research/pub/2023-SE.Component-based_CEGAR_Building_Software_Verifiers_from_Off-the-Shelf_Components.pdf}, abstract = {}, keyword = {CPAchecker,Software Model Checking,Cooperative Verification}, annote = {This is a summary of a <a href="https://www.sosy-lab.org/research/bib/Year/2022.html#ICSE22">full article on this topic</a> that appeared in Proc. ICSE 2022.}, doinone = {DOI not available}, isbnnote = {978-3-88579-726-5}, urlpub = {https://dspace.gi.de/handle/20.500.12116/40128}, }
    Additional Infos
    This is a summary of a full article on this topic that appeared in Proc. ICSE 2022.
  9. Maurice ter Beek, Rolf Hennicker, and José Proença. Realisability of Global Models of Interaction. In Proceedings of the International Colloquium on Theoretical Aspects of Computing (ICTAC) 2023, 2023. Link to this entry
    Abstract
    We consider global models of communicating agents specified as transition systems labelled by interactions in which multiple senders and receivers can participate. A realisation of such a model is a set of local transition systems—one for each agent—which are executed concurrently using synchronous communication. Our core challenge is how to check whether a global model is realisable and, if it is, how to synthesise a realisation. We identify and compare two variants to realise global interaction models, both relying on bisimulation equivalence. Then we investigate, for both variants, realisability conditions to be checked on global models. We propose a synthesis method for the construction of realisations by grouping locally indistinguishable states. The paper is accompanied by a tool that implements realisability checks and synthesises realisations.
    BibTeX Entry
    @inproceedings{HennickerICTAC23, author = {Maurice ter Beek and Rolf Hennicker and José Proença}, title = {Realisability of Global Models of Interaction}, booktitle = {Proceedings of the International Colloquium on Theoretical Aspects of Computing (ICTAC) 2023}, year = {2023}, abstract = {We consider global models of communicating agents specified as transition systems labelled by interactions in which multiple senders and receivers can participate. A realisation of such a model is a set of local transition systems—one for each agent—which are executed concurrently using synchronous communication. Our core challenge is how to check whether a global model is realisable and, if it is, how to synthesise a realisation. We identify and compare two variants to realise global interaction models, both relying on bisimulation equivalence. Then we investigate, for both variants, realisability conditions to be checked on global models. We propose a synthesis method for the construction of realisations by grouping locally indistinguishable states. The paper is accompanied by a tool that implements realisability checks and synthesises realisations.}, }
  10. Lenz Belzner, Thomas Gabor, and Martin Wirsing. Large Language Model Assisted Software Engineering: Prospects, Challenges, and a Case Study. In Bernhard Steffen, editors, Proc. AISoLA, LNCS 14380, 2023. Springer. Link to this entry To appear. PDF
    BibTeX Entry
    @inproceedings{WirsingAISoLA23, author = {Lenz Belzner and Thomas Gabor and Martin Wirsing}, title = {Large Language Model Assisted Software Engineering: Prospects, Challenges, and a Case Study}, booktitle = {Proc. AISoLA}, editor = {Bernhard Steffen}, year = {2023}, series = {LNCS~14380}, publisher = {Springer}, pdf = {https://sosy-lab.org/research/pub/2023-AISoLA.Large_Language_Model_Assisted_Software_Engineering.pdf}, note = {To appear.}, }
  11. Martin Wirsing and Lenz Belzner. Towards Systematically Engineering Autonomous Systems using Reinforcement Learning and Planning. In In Pedro López-García, John P. Gallagher, and Roberto Giacobazzi, editors, Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems - Essays Dedicated to Manuel Hermenegildo on the Occasion of His 60th Birthday, LNCS 13160, pages 281-306, 2023. Springer. doi:10.1007/978-3-031-31476-6_16 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{WirsingAVERTIS23, author = {Martin Wirsing and Lenz Belzner}, title = {Towards Systematically Engineering Autonomous Systems using Reinforcement Learning and Planning}, booktitle = {Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems - Essays Dedicated to Manuel Hermenegildo on the Occasion of His 60th Birthday}, editor = {In Pedro López-García and John P. Gallagher and Roberto Giacobazzi}, pages = {281--306}, year = {2023}, series = {LNCS~13160}, publisher = {Springer}, doi = {10.1007/978-3-031-31476-6_16}, pdf = {https://sosy-lab.org/research/pub/2023-AVERTIS.Towards_Systematically_Engineering_Autonomous_Systems_using_Reinforcement_Learning_and_Planning.pdf}, }

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

  1. Benedikt Damböck. Verification of Java Programs with Exceptions with CPAchecker. Master's Thesis, LMU Munich, Software Systems Lab, 2023. Link to this entry Keyword(s): CPAchecker, Software Model Checking PDF Presentation
    BibTeX Entry
    @misc{DamboeckJavaExceptions, author = {Benedikt Damböck}, title = {Verification of Java Programs with Exceptions with CPAchecker}, year = {2023}, pdf = {https://www.sosy-lab.org/research/msc/2023.Damboeck.Verification_of_Java_Programs_with_Exceptions_with_CPAchecker.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2023-12-06_MA_Verification_of_Java_Programs_with_Exceptions_with_CPAchecker_Damboeck.pdf}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
  2. Charlotte Gall. Updating the BenchExec Core Assignment for Modern CPU Architecture. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2023. Link to this entry Keyword(s): Benchmarking
    BibTeX Entry
    @misc{GallBenchexecCoreAssignment, author = {Charlotte Gall}, title = {Updating the BenchExec Core Assignment for Modern CPU Architecture}, year = {2023}, keyword = {Benchmarking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  3. Jens Linden. Scaling Formal Verification: Parallel Analysis of Functions in CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2023. Link to this entry
    BibTeX Entry
    @misc{LindenParallelAnalysis, author = {Jens Linden}, title = {Scaling Formal Verification: Parallel Analysis of Functions in CPAchecker}, year = {2023}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  4. Moritz Bierwirth. Designing and Assessing a Benchmark Set for Fault Localization Using Fault Injection. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2023. Link to this entry Keyword(s): Benchmarks PDF
    BibTeX Entry
    @misc{BierwirthFLBenchmarks, author = {Moritz Bierwirth}, title = {Designing and Assessing a Benchmark Set for Fault Localization Using Fault Injection}, year = {2023}, pdf = {https://www.sosy-lab.org/research/bsc/2023.Bierwirth.Designing_and_Assessing_a_Benchmark_Set_for_Fault_Localization_Using_Fault_Injection.pdf}, keyword = {Benchmarks}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  5. Salih Ates. Improving the Encoding of Arrays in Btor2-to-C Translation. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2023. Link to this entry Keyword(s): Btor2, Arrays PDF Presentation
    BibTeX Entry
    @misc{AtesBtor2CArray, author = {Salih Ates}, title = {Improving the Encoding of Arrays in Btor2-to-C Translation}, year = {2023}, pdf = {https://www.sosy-lab.org/research/bsc/2023.Ates.Improving_the_Encoding_of_Arrays_in_Btor2-to-C_Translation.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2023-08-30_BA_Improving_the_Encoding_of_Arrays_in_Btor2-to-C_Translation_Salih_Ates.pdf}, keyword = {Btor2, Arrays}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  6. Dusica Weisbarth. Ethics-based requirements analysis for a triage software: a case study. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2023. Link to this entry
    BibTeX Entry
    @misc{WeisbarthAnforderungsanalyse, author = {Dusica Weisbarth}, title = {Ethics-based requirements analysis for a triage software: a case study}, year = {2023}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }

Thesis defenses

  1. Winnie Lilith Sofia Ros. Extending the JavaSMT Framework with the Apron Library for Numerical Abstract Domain with subsequent Usability Assessment. Defense at LMU Munich, Bachelor's Thesis, LMU Munich, Software Systems Lab, 2023. Link to this entry Keyword(s): Apron, SMT, Abstract Interpretation, JavaSMT PDF
    BibTeX Entry
    @defense{RosBA, author = {Winnie Lilith Sofia Ros}, title = {Extending the JavaSMT Framework with the Apron Library for Numerical Abstract Domain with subsequent Usability Assessment}, year = {2023}, pdf = {2023.Ros.Extending_the_JavaSMT_Framework_with_the_Apron_Library_for_Numerical_Abstract_Domain_with_subsequent_Usability_Assessment.pdf}, keyword = {Apron, SMT, Abstract Interpretation, JavaSMT}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, venue = {LMU Munich}, }
  2. Daniel Raffler. Adding the SMT solver OpenSMT2 to the JavaSMT Framework and Evaluation using CPAchecker. Defense at LMU Munich, Bachelor's Thesis, LMU Munich, Software Systems Lab, 2023. Link to this entry Keyword(s): SMT, JavaSMT, OpenSMT2, CPAchecker PDF
    BibTeX Entry
    @defense{RafflerBA, author = {Daniel Raffler}, title = {Adding the SMT solver OpenSMT2 to the JavaSMT Framework and Evaluation using CPAchecker}, year = {2023}, pdf = {2023.Raffler.Adding_the_SMT_solver_OpenSMT2_to_the_JavaSMT_Framework_and_Evaluation_using_CPAchecker.pdf}, keyword = {SMT, JavaSMT, OpenSMT2, CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, venue = {LMU Munich}, }
  3. Janelle King. Implementing a Solver-Independent SMT-LIB2 Parser-Interpreter and Code-Generator for JavaSMT with Subsequent Evaluation. Defense at LMU Munich, Bachelor's Thesis, LMU Munich, Software Systems Lab, 2023. Link to this entry Keyword(s): JavaSMT, SMT-LIB2, SMT, CPAchecker PDF
    BibTeX Entry
    @defense{KingBA, author = {Janelle King}, title = {Implementing a Solver-Independent SMT-LIB2 Parser-Interpreter and Code-Generator for JavaSMT with Subsequent Evaluation}, year = {2023}, pdf = {2023.King.Implementing_a_Solver-Independent_SMT-LIB2_Parser-Interpreter_and_Code-Generator_for_JavaSMT_with_Subsequent_Evaluation.pdf}, keyword = {JavaSMT, SMT-LIB2, SMT, CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, venue = {LMU Munich}, }

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: Wed May 22 01:04:39 2024 UTC