News
Student talks at LMU
We regularly host student talks in the context of seminars, projects, and theses. All students and staff are welcome to participate. A list of all upcoming talks can be found in the talk schedule
News
-
2024-06-23
Our paper "A Transferability Study of Interpolation-Based Hardware Model Checking for Software Verification" received the ACM SIGSOFT Distinguished Paper Award and its reproduction artifact received the Best Artifact Award at FSE 2024! -
2024-06-13
Our papers "Software Verification with CPAchecker: Tutorial and User Guide" and "fm-weck: Containerized Execution of Formal Methods Tools" have been accepted at FM 2024! We will give a half-day tutorial on CPAchecker and look forward to your participation. -
2024-06-04
The following 3 papers got accepted: Paper accepted for LPAR 2024: R. Hennicker, A. Knapp, M. Wirsing: Symbolic Realisation of Epistemic Processes
Paper accepted for Coordination 2024: M. ter Beek, R. Hennicker, J. Proenca: Team Automata: Overview and Roadmap
Paper accepted for ICE 2024: F. Barbanera, R. Hennicker: Safe Composition of Systems of Communicating Finite State Machines
-
2024-05-01
We receive 5 Contributor Projects for Google Summer of Code 2024. We sincerely welcome Ahmed Tarek, Eshaan Aggarwal, Haoran Yang, Kerim Kochekov, and John Lu to work with us on exciting projects for BenchExec, Btor2-Cert, CPAchecker, and PJBDD. Learn more about their projects on our GSoC page. -
2024-04-15
Our papers "A Transferability Study of Interpolation-Based Hardware Model Checking for Software Verification" and "Decomposing Software Verification Using Distributed Summary Synthesis" have been accepted at FSE 2024! -
2024-04-11
The reproduction artifact of our paper "Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers" received the Distinguished Artifact Award at TACAS 2024! 
-
2024-04-10
Our paper "Augmenting Interpolation-Based Model Checking with Auxiliary Invariants" received the Best Paper Award at SPIN 2024! 
-
2024-04-09
The DFG research training group on Continuous Verification of CYber-Physical Systems (ConVeY) is looking for PhD students. Application deadline is April 21, 2024. Application Portal with more Information -
2024-02-27
Our papers "Augmenting Interpolation-Based Model Checking with Auxiliary Invariants", "Fault Localization on Verification Witnesses", "Software Verification Witnesses 2.0" (joint work with Masaryk University), and "Test-Case Generation with Automata-based Software Model Checking" have been accepted at SPIN 2024! -
2024-02-22
SoSy-Lab is again a mentoring organization of Google Summer of Code (GSoC) 2024. As a participant of GSoC, Google pays you for contributing to an open-source project. We provide interesting projects and expert mentorship for your participation. -
2024-02-06
Our competition contribution papers "CPAchecker 2.3 with Strategy Selection" and "CPV: A Circuit-Based Program Verifier" have been accepted at SV-COMP 2024! -
2024-01-13
Our paper "P3: A Dataset of Partial Program Patches" has been accepted at MSR 2024!
This is joint work with Moeketsi Raselimo and Lars Grunske. -
2023-12-22
Our paper "Tighter Construction of Tight Büchi Automata" has been accepted at FOSSACS 2024!
This is joint work with Jan Strejček. -
2023-12-22
Our paper "Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers" has been accepted at TACAS 2024! -
2023-11-08
We are very happy to announce that the joint research training group ConVeY (Continuous verification of cyber-physical systems) of LMU and TUM got extended by the Deutsche Forschungsgemeinschaft (DFG). That is, the research training group that started 2019 gets funding for additional four and half years. The complete press release of the DFG can be found here. -
2023-09-06
Our paper on "Deductive Verification of Leaked Information in Concurrent Applications" has been accepted at CCS 2023. Joint work by Toby Murray, Mukesh Tiwari, Gidon Ernst, and David Naumann. -
2023-07-31
Our paper on "Insecurity Separation Logic" has been accepted at ICFEM 2023. Joint work with Toby Murray and Pengbo Yan. -
2023-07-06
Our papers "CEGAR-PT: A Tool for Abstraction by Program Transformation", "CPA-DF: A Tool for Configurable Interval Analysis to Boost Program Verification", and "LIV: Invariant Validation Using Straight-Line Programs" have been accepted at ASE 2023! -
2023-05-04
We receive 4 Contributor Projects for Google Summer of Code 2023. We sincerely welcome Bas Laarakker, George Granberry, Jia Sun, and Julius Brehme to work with us on exciting projects for CPAchecker and JavaSMT. Learn more about their projects on our Google Summer of Code page. -
2023-05-02
Dirk Beyer and Stefan Löwe received the ETAPS Test-of-Time award ETAPS 2023 from Don Sannella, for their FASE'13 paper. Presentation at ETAPS'23: Slides
-
2023-02-22
As a participant of Google summer of code Google pays you for contributing to an open-source project. We provide projects and mentorship by experts for your potential participation. -
2023-01-20
Our paper "CoVeriTeam Service: Verification as a Service" has been accepted at ICSE 2023! -
2023-01-20
Our paper "Can we Communicate? Using Dynamic Logic to Verify Team Automata" (M. ter Beek, G. Cledou, R. Hennicker, J. Proenca) has been accepted at FM 2023! -
2023-01-12
Gidon Ernst receives the teaching award for methods in software engineering by the GAF: best master lecture 2022. -
2022-12-23
Our paper "Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Translator" has been accepted at TACAS 2023! -
2022-03-08
We are proud to announce that Prof. Dr. Dr. h.c. Martin Wirsing receives the Order of Merit of the Federal Republic of Germany (Bundesverdienstkreuz) from the president of Germany, Walter Steinmeier. (More Information) -
2022-03-07
The article Martin Wirsing and Dieter Frey: Agile governance for innovating higher education teaching and learning will be published in Rivista di Digital Politics. -
2022-02-16
The European Joint Conferences on Theory and Practice of Software (ETAPS) is an international association of conferences, which was founded in 1998 and has been held annually since then. The thematic orientation of the ETAPS ranges from fundamental aspects of software systems, computer-aided formal analysis and verification methods for software and hardware systems to practical aspects of programming and software engineering. This includes various aspects of the system development process, including specification, design, implementation, analysis, and maintenance, as well as the languages, methods, and tools necessary for these tasks. Different gradations of theory and practice are represented, on the one hand focused on theory with practical motivation, and on the other hand also on well-founded practice. Many of the issues in software development are relevant to systems in general, including hardware systems.
In 2022 ETAPS returns to Germany after 11 years. Prof. Kretinsky (TUM) and Prof. Beyer (LMU) have been appointed to organize the 25th edition of ETAPS in Munich, the first one held on site after the cancellation in 2020 and purely online event in 2021 due to Corona. All students and employees of TUM and LMU are cordially invited to attend the scientific program. (CoViD-related registration procedures might still be in place.) Attending the social events and coffee/lunch breaks requires a (paid) registration. The event is also supported by global industrial research leaders such as Google, Amazon, and Facebook, as well as successful companies with TUM roots, such as Celonis or Itestra.
The ETAPS conferences consist of ESOP (31st European Symposium on Programming), TACAS (28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems), FASE (25th International Conference on Fundamental Approaches to Software Engineering), and FoSSaCS (25th International Conference on Foundations of Software Science and Computation Structures). ETAPS 2022 will be accompanied by a series of scientific events, including 15 workshops, which will highlight a very broad spectrum of current research topics.
The main conferences will take place on TUM campus Garching from April 4 to April 7, preceded by the workshops on April 2 and 3. More information is available at https://etaps.org.
-
2022-02-14
Our paper "Decomposing Software Verification into Off-the-Shelf Components: An Application to CEGAR" has been accepted at ICSE 2022! -
2021-10-12
Loop Verification with Invariants and Contracts, paper accepted at VMCAI, extended version -
2021-07-22
Our article Falsification of Hybrid Systems Using Adaptive Probabilistic Search is published in the ACM Transactions on Modeling and Computer Simulation (TOMACS). Joint work with Sean Sedwards, Zhenya Zhang, and Ichiro Hasuo. -
2021-07-16
Our paper JavaSMT 3: Interacting with SMT Solvers in Java has been published at CAV 2021. -
2021-07-05
Our paper PJBDD: A BDD Library for Java and Multi-Threading has been accepted at ATVA 2021! The preprint is online (see link before). -
2021-04-25
Cooperative Verifier-Based Testing with CoVeriTest published in journal STTT. -
2021-04-21
Deductive Verification via the Debug Adapter Protocol, with J. Blau and T. Murray. Bringing deductive verification into your IDE! To be presented at F-IDE 2021 (colocated with NFM), current draft. -
2021-03-31
TACAS presentations on PDR for Software and CPU Energy Meter are available. -
2021-02-15
The journal article "Synthesizing Safe Policies under Probabilistic Constraints with Reinforcement Learning and Bayesian Model Checking" was published at Science of Computer Programming.
Two additional articles were published at ISoLA\20: "A Dynamic Logic for Systems with Predicate-Based Communication"
and "Rigorous Engineering of Collective Adaptive Systems Introduction to the 3rd Track Edition" . -
2021-02-07
Competition Reports for SV-COMP 2021 and Test-Comp 2021 available: SV-COMP 2021 and Test-Comp 2021 -
2020-12-23
The paper "Bridging Arrays and ADTs in Recursive Proofs" was accepted at TACAS'21. Joint work with Grigory Fedyukovich. -
2020-11-01
The LMU Research Award (LMU Forschungspreis) was awarded to Matthias Kettl for his Bachelor Thesis on Fault Localization for Formal Verification. We are proud to have supervised him. Matthias will continue his Master studies at LMU and continue his work as a working student at our chair. -
2020-10-29
Our paper "Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization" has been accepted at ESEC/FSE 2020! The preprints are online (see links before). -
2020-08-18
Our three papers "An Interface Theory for Program Verification", "Verification Artifacts in Cooperative Verification", and "Violation Witnesses and Result Validation for Multi-Threaded Programs" have been accepted at ISoLA 2020! The preprints are online (see links before). -
2020-08-03
Our two papers "Difference Verification with Conditions" and "FRed: Conditional Model Checking via Reducers and Folders" have been accepted at SEFM 2020! The preprints are online (see links before). -
2020-07-30
The paper "Legion: Best-First Concolic Testing" has been accepted at ASE 2020. See also Test-Comp 2020. Joint work with Dongge Liu, Toby Murray, and Ben Rubinstein from the University of Melbourne. -
2020-07-24
-
2020-04-25
-
2020-02-24
Our paper about our tool CPU Energy Meter has been accepted at TACAS 2020! The preprint is now online. -
2019-12-20
9th Competition on Software Verification (SV-COMP 2020) has announced the results. Congratulations to all participants and winners! Results are available on the competition web site -
2019-11-21
Gastvorträge am 27.11.: Klimawandel und Extremereignisse – neue Erkenntnisse für die Klimafolgenforschung durch die Nutzung von HPC. Prof. Dr. Ralf Ludwig um 9:15 im Rahmen der Vorlesung Softwaretechnik, sowie Andrea Böhnisch und Magdalena Mittermeier um 14:15 im Rahmen der Vorlesung Einführung in die Informatik: Programmierung und Softwareentwicklung. Vielen herzlichen Dank an Students for Future Munich für die Organisation. Beide Vorträge sind öffentlich (Hauptgebäude Geschwister Scholl Platz 1, A240). -
2019-09-18
Our paper TestCov: Robust Test-Suite Execution and Coverage Measurement has been accepted for presentation at ASE 2019 -
2019-09-16
Paper Behavioural and Abstractor Specifications for a Dynamic Logic with Binders and Silent Transitions accepted for presentation at DaLi 2019 -
2019-08-03
Paper Conditional Testing: Off-the-Shelf Combination of Test-Case Generators accepted for presentation at ATVA 2019 -
2019-07-26
Registration for the 4th International Workshop on CPAchecker on 1st and 2nd Oct. is open! It will be held on the island Frauenchiemsee near Munich, Germany. Participation is open to everbody!
Registration via Google form, open until 8th August -
2019-07-12
The DFG research training group ConVeY started on July 1st. The kick-off meeting was on July 12 -
2019-05-06
We welcome Aditya Arora, Saheed Bolarinwa, and Tharsanan Kurukulasingam, who will be working with us this summer on exciting projects for BenchExec, JavaSMT, and CPAchecker. Read about their projects on our Google Summer of Code page -
2019-04-17
The paper SecCSL: Security Concurrent Separation Logic by Gidon Ernst (joint work with Toby Murray) was accepted at CAV19. 
Paper Draft, Website: SecC
-
2019-04-09
Publication on "CoVeriTest: Cooperative Verifier-Based Testing by Dirk Beyer and Marie-Christine Jakobs at FASE19! Marie-Christines presentation is a must: Thursday, 11th April, at 16:30, room Jupiter. -
2019-04-09
Slides to the ETAPS19 tutorial on Software Verification: "An Overview of the State of the Art" are available here. -
2019-02-28
SoSy-Lab was once again selected as an organization of Google Summer of Code.
Students can apply from March 25 to April 9, 2019 - get into contact now! (General Information, Possible projects) -
2019-02-28
Our tool CPAchecker defended the title: it wins category Overall and 6 more medals" in the 8th Competition on Software Verification (SV-COMP19). -
2018-05-04
Our tool CPAchecker wins category Overall and 5 more medals in the 7th Competition on Software Verification (SV-COMP18).
-
2018-02-27
SoSy-Lab was selected as an organization for the" Google Summer of Code and will mentor two students working on the CPAchecker project.