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"

Prof. Dr. Dirk Beyer

Full Professor, Head of Research Chair (Lehrstuhlinhaber)

Picture of Prof. Dr. Dirk Beyer

Software and Computational Systems Lab
Institute for Informatics
Ludwig-Maximilians-Universität München (LMU Munich)
Oettingenstraße 67
80538 Munich (Germany)

Room 062, Oettingenstr. 67
Office hours
Mi 10-11, and by appointment
+49 (89) 2180-9150 (Sec.: -9151)
+49 (89) 2180-9175


Please send me encrypted mails!
My GPG key: 0xFA7541D4 (from key server)
Fingerprint: D01F 72A6 EF21 E258 BEF5 2D02 96A2 AE57 FA75 41D4

Personals Publications, DBLP, Google Scholar, ORCID, Semantic Scholar, ACM
Biographical sketch
Curriculum vitae
You can also follow me on Twitter and Google+.
NEW Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework (ISoLA 2020)
An Interface Theory for Program Verification (ISoLA 2020)
Violation Witnesses and Result Validation for Multi-Threaded Programs (ISoLA 2020)
Difference Verification with Conditions (SEFM 2020)
FRed: Conditional Model Checking via Reducers and Folders (SEFM 2020)
MetaVal: Witness Validation via Verification (CAV 2020)
Software Verification with PDR: An Implementation of the State of the Art (TACAS 2020)
CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering (TACAS 2020)
Second Competition on Software Testing: Test-Comp 2020 (FASE 2020)
Advances in Automatic Software Verification: SV-COMP 2020 (TACAS 2020)
Research I am one of the PIs of the Research Training Group ConVeY (DFG-Graduiertenkolleg).
My research focuses on models, algorithms, and tools for the construction and analysis of reliable software systems, in particular:
Interfaces for component-based design (download Chic)
Software model checking and static analysis (download CPAchecker, BLAST, CSIsat)
Structure analysis and comprehension of large systems (download CrocoPat or CCVisu)
Formal verification of real-time systems (download Rabbit)
Service 3rd Intl. Competition on Software Testing (Test-Comp '21)
10th Intl. TACAS Competition on Software Verification (SV-COMP '21)
PC Chair: VMCAI 2020 (Jan 19-21, 2020, New Orleans, USA)
PC Chair: TAP 2019 (Oct 9-11, 2019, Porto, Portugal)
4th Intl. Workshop on CPAchecker (CPA '19)
PC Chair: TACAS 2018
1st Intl. Workshop on CPAchecker (CPA'16)
CAV 2015 Workshops
Program committees: ICSME'15, TAP'15, ICPC'15, FMSPLE'15, NFM'15, SPIN'14, FMCAD'14, FORTE'14
... more
Courses offered: current term, next term
... more
People Team
Information for prospective students
Technical hints for writing a paper
Software that I use
Software BenchExec: Reliable Benchmarking and Resource Measurement
BLAST: Model Checking of Software
CCVisu: Visual Clustering and Software-Structure Assessment
CheckDep: Tracking Software Dependencies
Chic: Checking Interface Compatibility
CPAchecker: Configurable Software Verification
CrocoPat: Relational Programming (for Software-Structure Analysis)
CSIsat: Interpolation for LA+EUF
DepDigger: Detecting Complex Low-Level Dependencies
JavaSMT: A Unified Interface for SMT Solvers in Java
Rabbit: Verification of Real-Time Systems
... more