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: Heizmann:Matthias
Contributed to:
2015
2015
2015
20152014201420132013
2010
20102009
20162017
2018Wrote 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.
- POPL-2010-HeizmannHP
- 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.