BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Austria
1 × Russia
1 × Spain
1 × United Kingdom
2 × Italy
2 × USA
3 × France
Collaborated with:
A.Podelski J.Hoenicke D.Dietsch J.Leike B.Musa D.Beyer M.Dangl N.D.Jones A.Nutz V.Langenfeld J.Christ M.Lindenmann C.Schilling A.Stahlbauer A.Farzan Z.Kincaid Y.Chen O.Lengál Yong Li 0031 M.Tsai A.Turrini L.Z.0001 S.Wissert E.Ermis
Talks about:
softwar (4) termin (4) check (4) autom (4) contribut (3) interpol (3) competit (3) program (3) ultim (3) model (3)

Person: Matthias Heizmann

DBLP DBLP: Heizmann:Matthias

Contributed to:

CAV 20152015
ESEC/FSE 20152015
LATA 20152015
TACAS 20152015
CAV 20142014
TACAS 20142014
CAV 20132013
TACAS 20132013
POPL 20102010
SAS 20102010
SAS 20092009
FSE 20162016
ESEC/FSE 20172017
PLDI 20182018

Wrote 15 papers:

CAV-2015-DietschHLP #approach #ltl #model checking #modulo theories
Fairness Modulo Theory: A New Approach to LTL Software Model Checking (DD, MH, VL, AP), pp. 49–66.
ESEC-FSE-2015-0001DDHS #validation #verification
Witness validation and stepwise testification across software verifiers (DB, MD, DD, MH, AS), pp. 721–733.
LATA-2015-FarzanHHKP #automation #verification
Automated Program Verification (AF, MH, JH, ZK, AP), pp. 25–46.
TACAS-2015-HeizmannDLMP #array #contest
Ultimate Automizer with Array Interpolation — (Competition Contribution) (MH, DD, JL, BM, AP), pp. 455–457.
CAV-2014-HeizmannHP #analysis #learning #source code #termination
Termination Analysis by Learning Terminating Programs (MH, JH, AP), pp. 797–813.
TACAS-2014-HeizmannCDHLMSWP #contest #satisfiability
Ultimate Automizer with Unsatisfiable Cores — (Competition Contribution) (MH, JC, DD, JH, ML, BM, CS, SW, AP), pp. 418–420.
TACAS-2014-LeikeH #linear #ranking
Ranking Templates for Linear Loops (JL, MH), pp. 172–186.
CAV-2013-HeizmannHP #automaton #model checking #people
Software Model Checking for People Who Love Automata (MH, JH, AP), pp. 36–52.
TACAS-2013-HeizmannCDEHLNSP #contest
Ultimate Automizer with SMTInterpol — (Competition Contribution) (MH, JC, DD, EE, JH, ML, AN, CS, AP), pp. 641–643.
Nested interpolants (MH, JH, AP), pp. 471–482.
SAS-2010-HeizmannJP #invariant #termination
Size-Change Termination and Transition Invariants (MH, NDJ, AP), pp. 22–50.
SAS-2009-HeizmannHP #abstraction #refinement
Refinement of Trace Abstraction (MH, JH, AP), pp. 69–85.
FSE-2016-BeyerDDH #correctness #verification
Correctness witnesses: exchanging verification results between verifiers (DB, MD, DD, MH), pp. 326–337.
ESEC-FSE-2017-DietschHMNP #model checking
Craig vs. Newton in software model checking (DD, MH, BM, AN, AP), pp. 487–497.
PLDI-2018-ChenHLLTTZ #algorithm #termination
Advanced automata-based algorithms for program termination checking (YFC, MH, OL, YL0, MHT, AT, LZ0), pp. 135–150.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.