Contact & Address
PGP Public Key: 0xD8BF1A0B19A1702D
Fingerprint: 36E9 C2E7 CF98 ACF5 BE5C 6EC2 D8BF 1A0B 19A1 702D
Software add Computational Systems Lab
Institute for Informatics
LMU Munich
Room: F 010
Oettingenstraße 67
80538 Munich (Germany)
Teaching
LMU Munich:
- SS 2017: SWEP
University of Passau:
- WS 2016/17: Software Engineering Praktikum
- SS 2016: Software Engineering Praktikum, Algorithmen und Datenstrukturen (Übung)
- WS 2015/16: Software Engineering Praktikum, Spezifikation und Verifikation von Eingebetteten Systemen (Übung)
- WS 2014/15: Software Engineering Praktikum, Spezifikation und Verifikation von Eingebetteten Systemen (Übung)
- WS 2013/14: Software Engineering Praktikum, Programmierung 2 (Korrektur)
- WS 2012/13: Haskell-Tutorium
Projects
Publications
List at DBLP-
Dirk Beyer,
Matthias Dangl,
Daniel Dietsch, and
Matthias Heizmann.
Correctness Witnesses: Exchanging Verification Results between Verifiers.
In
J. Cleland-Huang and Z. Su, editors,
Proc. FSE,
2016.
ACM, New York.
[
PDF
]
-
Dirk Beyer and
Matthias Dangl.
Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses.
In
S. Chaudhuri and A. Farzan, editors,
Proc. CAV,
2016.
Springer-Verlag, Heidelberg.
[ PDF
]
-
Dirk Beyer and
Matthias Dangl.
SMT-based Software Model Checking: An Experimental Comparison of Four Algorithms.
In
M. Chechik and T. Kahsai, editors,
Proc. VSTTE,
2016.
Springer-Verlag, Heidelberg.
[ PDF
]
-
Dirk Beyer,
Matthias Dangl,
Daniel Dietsch,
Matthias Heizmann, and
Andreas Stahlbauer.
Witness Validation and Stepwise Testification across Software Verifiers.
In
E. Di Nitto, M. Harman, and P. Heymans, editors,
Proc. ESEC/FSE,
2015.
ACM, New York.
[ PDF
] Keywords: Error Witness, Counterexample Validation, Software Verification, Program Analysis, Model Checking
-
Dirk Beyer,
Matthias Dangl, and
Philipp Wendler.
Boosting k-Induction with Continuously-Refined Invariants.
In
D. Kroening and C. S. Pasareanu, editors,
Proc. CAV,
LNCS 9206,
2015.
Springer-Verlag, Heidelberg.
[ PDF
] Keywords: Software Model Checking, k-Induction, Invariant Generation.
- Matthias Dangl, Stefan Löwe, and Philipp Wendler. CPAchecker with support for recursive programs and floating-point arithmetic. In Proc. TACAS, LNCS, 2015. Springer-Verlag, Heidelberg. Keywords: Software Model Checking, k-Induction, Predicate Abstraction, Value Analysis, SV-COMP