Matthias Heizmann
Matthias Heizmann
University of Freiburg
Georges-Köhler-Allee 52
79110 Freiburg
|
Research
Short: software verification. More detailed: I am working on automatic methods that verify safety and liveness properties of sequential and concurrent programs. My research interests include also automata theory, formal language theory, synthesis of termination arguments and interpolant generation.
I am investigating a verification technique in which a system can be considered as an intersection of languages. In this setting, verification problems can be reduced to well-known descision problems of languages. The crux of the approach is to abstract complex languages by more tractable languages. To refine such an abstraction automatically, I am investigating a technique in which automata are constructed from interpolants that are derived from spurious counterexamples.
Parts of my research are implemented in Ultimate Automizer, which is one toolchain of the Ultimate Program Analysis Framework.
Teaching
- Lecture: Program Verification (Summer Term 2021)
- Seminar: Advanced Topics in Program Analysis (Winter Term 2020/21)
- Lecture: Program Verification (Summer Term 2020)
- Seminar: Automata Theory (Winter Term 2019/20)
- Lecture: Program Verification (Summer Term 2019)
- Lecture: Theoretical Computer Science (Winter Term 2018/19)
- Lecture: Theoretical Computer Science (Winter Term 2017/18)
Student Projects
Publications
You can find an updated list at DBLP and Google Scholar, below is a selection of older papers.
- Geometric Series as Nontermination Arguments for Linear Lasso Programs, in WST 2014, together with Jan Leike [preprint]
- Termination Analysis by Learning Terminating Programs, in CAV 2014, together with Jochen Hoenicke and Andreas Podelski [preprint]
- Ranking Templates for Linear Loops, in TACAS 2014, together with Jan Leike [bib | preprint]
- Ultimate Automizer with Unsatisfiable Cores - (Competition Contribution), in TACAS 2014, together with Jürgen Christ, Daniel Dietsch, Jochen Hoenicke, Markus Lindenmann, Betim Musa, Christian Schilling, Stefan Wissert, and Andreas Podelski [bib]
- Linear Ranking for Linear Lasso Programs, in ATVA 2013, together with Jochen Hoenicke, Jan Leike, and Andreas Podelski. [bib| preprint]
- Ultimate Automizer with SMTInterpol - (Competition Contribution), in TACAS 2013, together with Jürgen Christ, Daniel Dietsch, Evren Ermis, Jochen Hoenicke, Markus Lindenmann, Alexander Nutz, Christian Schilling, and Andreas Podelski. [bib]
- Software Model Checking for People Who Love Automata, in CAV 2013, together with Jochen Hoenicke and Andreas Podelski [bib | preprint]
- Size-Change Termination and Transition Invariants , in SAS 2010, together with Neil D. Jones and Andreas Podelski. [ bib | pdf ]
- Nested interpolants, in POPL 2010, together with Jochen Hoenicke and Andreas Podelski. [bib | pdf]
- Refinement of Trace Abstraction, in SAS 2009, together with Jochen Hoenicke and Andreas Podelski.
[bib | pdf]
Talks and Posters (to be updated...)
- Termination Analysis by Learning Terminating Programs, July 2014, at CAV 2014
- Geometric Series as Nontermination Arguments for Linear Lasso Programs, July 2014, at WST 2014
- Ultimate Automizer Poster, April 2014, at TACAS 2014 and Dagstuhl Seminar 14171
- Ultimate Automizer with Unsatisfiable Cores, April 2014, at TACAS 2014
- Ranking Templates for Linear Loops, April 2014, at TACAS 2014.
- Trace Abstraction, November 2010, at Department of Computer Science and Automation, Indian Institute of Science, Bangalore.
- Nested Interpolants, January 2010, at POPL 2010.
- Refinement of Trace Abstraction, August 2009, at SAS 2009, presented by Jochen Hoenicke.
- Trace Abstraction, March 2009, at R1 meeting of the AVACS Workshop Spring 2009 in Freiburg.
Available on request, but I suggest to have a look at the slides of the SAS09 talk which is an improved and extended version based on this talk. - Regular Abstraction, Oktober 2008, at Software Analysis Workshop in Alacati.
I suggest to have a look at the slides of the SAS09 talk which is an improved and extended version based on this talk. - My Talk at the Abstract Interpretation Seminar in Winter Term 07/08, about Fixpoint-Guided Abstraction Refinements (which was published by Patrick Cousot, Pierre Ganty and Jean-François Raskin in SAS 2007)
- My Talk at the Advanced Topics in Model Checking Seminar in Summer Term 2007, about Constructive Versions of Tarski's Fixed Point Theorems (which was published by Patrick Cousot & Radhia Cousot in Pacific Journal of Mathematics, Vol. 82)