Benchmarking and Preserving Tools for Formal Methods.
Invited talk at Computing Colloquium of College of Engineering,
05. September 2025.
The Transformation Game: Joining Forces for Verification (Keynote).
Invited talk at 46th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2025),
25. June 2025.
FM-Tools: A Library of Tools for Formal Methods — Find, Use, Conserve, Execute (Lecture 3).
Invited talk at Summer School on Fuzzing and Security,
28. May 2025.
The Transformation Game: Joining Forces for Verification (Lecture 2).
Summer School on Fuzzing and Security,
28. May 2025.
Software Verification with CPAchecker (Lecture 1).
Summer School on Fuzzing and Security,
28. May 2025.
A Unifying View on SMT-Based Software Verification (Guest Lecture).
NTU Course,
22. April 2025.
Reliable Benchmarking: Requirements and Solutions.
Johannes Keppler University Linz,
25. October 2024.
Towards Scalable and Distributed Software Verification.
Huawei Workshop on Formal Methods,
18. September 2024.
Towards Scalable and Distributed Software Verification.
Alpine Verification Meeting,
04. September 2024.
Reliable Benchmarking: Requirements and Solutions.
Guest lecture at KIT,
03. September 2024.
Distributed Automatic Contract Construction.
Keynote at the KeY Symposium 2025,
31. July 2024.
Explicit-State Software Model Checking Based on CEGAR and Interpolation (Test-of-Time Award Presentation).
ETAPS 2023 – European Joint Conferences on Theory and Practice of Software,
27. April 2023.
Benchmarking in Computer Science and Competition on Software Verification.
Masaryk University, Brno,
21. March 2023.
Verification Tools, Exchange Formats, and Combination Approaches.
Euro Proof Net WG3 Cost Action 2023,
8. February 2023.
Cooperative Verification.
SBMF 2022,
9. December 2022.
Cooperative Verification: Towards Reliable Safety-Critical Systems.
FTSCS 2022,
7. December 2022.
Cooperative Software Verification: Combination Approaches that Share Information.
Research Seminar at University of Wellington,
18. November 2022.
Software Verification and Verification Witnesses.
Huawei Workshop 2022,
11. October 2022.
Cooperative Software Verification:
Combination Approaches that Share Information (Guest Lecture).
Manchester University,
Manchester, UK, 2022-08-16.
Reliable Benchmarking: Requirements and Solutions (Guest Lecture).
Manchester University,
Manchester, UK, 2022-08-16.
Interpolation and SAT-Based Model Checking Revisited:
Adoption to Software Verification.
Isaac Newton Institute for Mathematics, Program Verified Software,
Cambridge, UK, 2022-07-22.
Cooperative Software Verification
Combination Approaches that Share Information.
Isaac Newton Institute for Mathematics, Program Verified Software,
Cambridge, UK, 2022-07-07.
Configurable Software Model Checking: CPAchecker.
Workshop at Amazon Web Services 2022,
Dresden, Germany, 2022-06-08.
Modular Model Checking (Frameworks).
Open Source Model Checker (Research Seminar at Iowa State University), Work Meeting,
Virtual, 2022-03-29.
CoVeriTeam: Cooperative Verification via Off-the-Shelf-Components.
ConVeY Research Graduate School,
Raitenhaslach, Germany, 2021-10-22.
PDR for Software.
TACAS Conference,
Virtual, 2021-03-31.
Software Verification — An Overview of the State of the Art.
Invited Talk at the European Joint Conferences on Theory and Practice of Software 2019,
Prague, Czechia, 2019-04-09.
Reducer-Based Construction of Conditional Model Checkers.
CPAchecker Workshop 2018,
2018-09-25.
Cooperative Verification: The Art of Combining Verification Tools.
fortiss (Forschungsinstitut des Freistaats Bayern für
softwareintensive Systeme und Services),
Munich, Germany, 2018-07-27.
Cooperative Verification: The Art of Combining Verification Tools.
Universität Konstanz,
Konstanz, Germany, 2018-07-19.
Cooperative Verification: The Art of Combining Verification Tools.
Keynote at the 12th International Conference on Tests and Proofs,
Toulouse, France, 2018-06-27.
Cooperative Verification: The Art of Combining Verification Tools.
Lectures at Eighth Summer School on Formal Techniques,
Menlo College, Atherton (CA), USA, 2018-05-23 – 2018-05-24.
Forschungswettbewerb als Motor des Technologie-Transfers.
Invited Talk at Dagstuhl Seminar,
Dagstuhl, Germany, 2018-04-11.
Verification with Reusing Exchangeable Results.
Lectures at RiSE/SHiNE Winter School,
TU Wien, Austria, 2018-02-08 – 2018-02-09.
Configurable Software Verification.
Lectures at RiSE/SHiNE Winter School,
TU Wien, Austria, 2018-02-08 – 2018-02-09.
Best Practices On Artifact Integration.
ACM Task Force Workshop on Reproducibility and Artifacts,
ACM Headquarter, New York, NY, USA, 2017-12-07.
Getting Software Verifiers Ready for Industrial Use.
Lectures at SOAMED Project Meeting,
Zeuthen, Germany, 2017-10-05.
Protocol Interfaces.
Workshop on Foundations of Interface Technologies,
Paris, 2010-08-30.
Adjustable-Block Encoding — Towards a Unified Framework for Software Verification. Computer Science Symposium at
IST Austria,
Klosterneuburg, 2010-05-07.
Program Analysis with Dynamic Change of Precision. University of California,
Berkeley (CA), 2009-04-16.
Efficient BDD Representation for Reachability Analysis of Timed Automata. Carnegie Mellon University, Pittsburgh (PA), 2003-01-14.
A Modular Approach for Formal Verification of Real-Time Systems. Software Engineering Institute, Pittsburgh (PA), 2003-01-10.
Improvements in BDD-based Reachability Analysis of Timed Automata. Naval Research Laboratory, Washington (D.C.), 2001-04-23.
Entwurfsmuster: Eine Einführung.
PC-Soft GmbH, Senftenberg, 1997-12-16.
Conference and Other Presentations
Certifying Software Verification.
Dagstuhl Seminar on Certifying Algorithms for Automated Reasoning,
3. June 2025.
Advances in Automatic Software Testing: Test-Comp 2025.
FASE,
8. May 2025.
Improvements in Software Verification and Witness Validation: SV-COMP 2025.
TACAS,
5. May 2025.
FM-Tools: Find, Use, and Conserve Tools for Formal Methods.
Dagstuhl Seminar on Information Exchange between Verifiers,
24. April 2025.
Improvements in Software Verification and Witness Validation: SV-COMP 2025.
SV-COMP Workshop at Frauenchiemsee, Germany,
1. April 2025.
Software Verification with CPAchecker 3.0: Tutorial and User Guide.
FM 2024,
10. September 2024.
The Next Decade of the CPAchecker Development Process.
9th International Workshop on CPAchecker (CPA 2024),
9. September 2024.
Extending the MoXI Eco System.
OSSyM,
21. July 2024.
Find, Use, and Conserve Tools for Formal Methods.
Podeski65,
25. June 2024.
Fault Localization on Verification Witnesses (Poster Paper).
ICSE 2024,
14. April 2024.
Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Translator.
AVM,
13. September 2023.
Software Model Checking: 20 Years and Beyond.
8th International Workshop on CPAchecker (CPA 2023),
11. September 2023.
Cooperative Verification.
Dagstuhl on Abstract Interpretation,
11. July 2023.
5th Competition on Software Testing.
FASE 2023,
27. April 2023.
5th Competition on Software Testing.
ETAPS 2023 – European Joint Conferences on Theory and Practice of Software,
26. April 2023.
12th Competition on Software Verification.
ETAPS 2023 – European Joint Conferences on Theory and Practice of Software,
26. April 2023.
TOOLympics 2023: Competitions in Formal Methods.
ETAPS 2023 – European Joint Conferences on Theory and Practice of Software,
26. April 2023.
12th Competition on Software Verification.
TACAS 2023,
24. April 2023.
12th Competition on Software Verification.
TACAS 2023,
24. April 2023.
CPAchecker (Competition Contribution for SV-COMP ’23).
TACAS 2023,
24. April 2023.
5th Competition on Software Testing (TEST-COMP ’23).
FASE 2023,
24. April 2023.
A Library of Formal-Methods Tools.
COOP 2023,
23. April 2023.
Case Study on Verification-Witness Validators: Where We Are and Where We Go.
SAS 2022,
5. December 2022.
Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization.
ESEC/FSE 2022,
15. November 2022.
Current Trends in CPAchecker.
CPAchecker Workshop 2022,
05. October 2022.
An Interface Theory for Program Verification.
ISOLA Conference,
Rhodos, Greece, 2021-10-29.
Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework.
ISOLA Conference,
Rhodos, Greece, 2021-10-29.
Violation Witnesses and Result Validation for Multi-threaded Programs: Implementation and Evaluation with CPAchecker.
ISOLA Conference,
Rhodos, Greece, 2021-10-25.
Software Verification: Historical Landmarks and Current Developments.
6th International Workshop on CPAchecker (CPA 2021),
Virtual, 2021-10-01.
Verification Witnesses — A Data Show Case.
MSR 2019,
Montreal, Canada, 2019-05-25.
Test-Comp at TOOLympics.
TOOLympics 2019 at ETAPS,
Prague, Czechia, 2019-04-07.
SV-COMP at TOOLympics.
TOOLympics 2019 at ETAPS,
Prague, Czechia, 2019-04-07.
1st Competition on Software Testing.
Test-Comp 2019,
Prague, Czechia, 2019-04-06.
Competition on Software Verification 2019.
SV-COMP 2019,
Prague, Czechia, 2019-04-06.
Applying CPAchecker to Large Explicit State Spaces.
RERS at ISOLA Conference,
2018-11-08.
In-Place vs. Copy-on-Write CEGAR Refinement for Block Summarization with Caching.
ISOLA Conference,
2018-11-06.
Strategy Selection.
ISOLA Conference,
2018-11-05.
Software Verification with Validation of Results.
TACAS Conference, SV-COMP Session,
Uppsala, Sweden, 2016-04-27.
Partial Verification and Intermediate Results as a Solution to
Combine Automatic and Interactive Verification Techniques.
ISOLA Conference,
2016-10.
Symbolic Execution with CEGAR.
ISOLA Conference,
2016-10-10.
Software Verification and Verifiable Witnesses.
21st International Conference on Tools and Algorithms for the Construction and of Analysis Systems TACAS 2015, London, UK, 2015-04-16.
Status Report on Software Verification.
20th International Conference on Tools and Algorithms for the Construction and of Analysis Systems TACAS 2014, Grenoble, France, 2014-04-10.
Second Competition on Software Verification.
19th International Conference on Tools and Algorithms for the Construction and of Analysis Systems TACAS 2013, Rome, 2013-03-21.
Competition on Software Verification.
18th International Conference on Tools and Algorithms for the Construction and of Analysis Systems TACAS 2012, Tallinn, 2012-03-29.
CPAchecker: A Tool for Configurable Software Verification.
23rd International Conference on Computer Aided Verification CAV 2011, Snowbird (UT), 2011-07-19.
CPAchecker: A Tool for Configurable Software Verification.
15th Biennial Workshop on Programmiersprachen und Grundlagen der Programmierung KPS 2009, Maria Taferl, 2009-10-14.
Evolution Storyboards: Visualization of Software Structure Dynamics.
14th International Conference on Program Comprehension ICPC 2006, Athens, 2006-06-16.
Co-change Visualization Applied to PostgreSQL and ArgoUML.
3rd International Workshop on Mining Software Repositories MSR 2006, Shanghai, 2006-05-23.
Co-Change Visualization.
21st IEEE International Conference on Software Maintenance ICSM 2005, Budapest, 2005-09-26.
Clustering Software Artifacts Based on Frequent Common Changes.
13th IEEE International Workshop on Program Comprehension IWPC 2005, St. Louis, 2005-05-16.
CrocoPat: An Efficient Calculator for Relational Programs. TRESOR seminar, EPFL, Lausanne, 2005-04-14.
An Introduction to Binary Decision Diagrams.
CAV lecture, EPFL, Lausanne, 2004-11-18.
An Eclipse Plug-in for Model Checking.
12th IEEE International Workshop on Program Comprehension IWPC 2004, Bari, 2004-06-26.
Generating Tests from Counterexamples.
26th International Conference on Software Engineering ICSE 2004, Edinburgh, 2004-05-27.
Generating Tests from Counterexamples. EPFL, Lausanne, 2004-05-18.
Simple and Efficient Relational Querying. OSQ seminar, University of California, Berkeley (CA), 2004-02-02.
How to Make Model Checking of Timed Automata Efficient. University of California, Berkeley (CA), 2003-10-29.
Rabbit: A Tool for BDD-based Verification of Real-Time Systems.
15th International Conference on Computer Aided Verification CAV 2003, Boulder (CO), 2003-07-09.
CrocoPat: Efficient Pattern Analysis in Object-Oriented Programs.
11th IEEE International Workshop on Program Comprehension IWPC 2003, Portland (OR), 2003-05-11.
Efficient Reachability Analysis and Refinement Checking of Timed Automata using BDDs.
11th IFIP Working Conference on Correct Hardware Design and Verification Methods CHARME 2001, Livingston, 2001-09-04.
Verification of Real-Time Systems.
Workshop on Real-Time Tools
RT-TOOLS 2001, Aalborg, 2001-08-20.
Efficient Verification of Timed Automata using BDDs.
6th International ERCIM Workshop on Formal Methods for Industrial Critical Systems
FMICS 2001, Paris, 2001-07-16.
Different Strategies for BDD-based Reachability Analysis of Timed Automata.
2nd IEEE/IFIP Joint Workshop on Formal Specifications of Computer-Based Systems
FSCBS 2001, Washington (D.C.), 2001-04-20.
Cottbus Timed Automata: Formal Definition and Semantics.
2nd IEEE/IFIP Joint Workshop on Formal Specifications of Computer-Based Systems
FSCBS 2001, Washington (D.C.), 2001-04-20.
Improvements in BDD-based Reachability Analysis of Timed Automata.
10th International Symposium of Formal Methods Europe FME 2001, Berlin, 2001-03-15.
A Tool for Modular Modelling and Verification of Hybrid Systems.
25th IFAC/IFIP Workshop on Real-Time Programming WRTP 2000, Palma, 2000-05-19.
Modular Modelling and Verification with Cottbus Timed Automata.
IEEE/IFIP Joint Workshop on Formal Specifications of Computer-Based Systems
FSCBS 2000, Edinburgh, 2000-04-06.
Modelling and Analysing a Railroad Crossing in a Modular Way.
5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems FMICS 2000, Berlin, 2000-04-04.
Concepts of Cottbus Timed Automata.
Workshop Formale Beschreibungstechniken für verteilte Systeme FBT 1999, München, 1999-06-17.
Ein Analysewerkzeug für zeitbehaftete Automaten.
Diplomarbeit, Cottbus, 1998-06-30.
Modeling a Production Cell as a Distributed Real-Time System with Cottbus Timed Automata.
Workshop Formale Beschreibungstechniken für verteilte Systeme FBT 1998, Cottbus, 1998-06-04.