Christoph M. Wintersteiger

---

Post-doctoral researcher in the Constraint Reasoning Group at Microsoft Research.

• Dr. sc. ETH Zurich, 2011
  (with Daniel Kroening and the Formal Verification Group)
  
• Dipl.-Ing. University of Linz, 2006
  (with Josef Scharinger)

• The Z3 Theorem Prover and SMT Solver
  I work on finite-domain decision procedures. Sound, complete and efficient.
• DeSAT
  Parallel and distributed SAT solvers that aim to solve bigger problems faster.

Past Projects

• squolem/qbv
  When you can't trust your QBF solver, you'll need certificates. I did a few experiments on that.
• SATABS/CBMC: goto-cc
  I wrote a compiler for model files to simplify software verification with our model checkers.
• Loopfrog
  A static analyzer that summarizes loops based on abstract interpretation principles.
• Termination
  I took a closer look at ranking function synthesis and termination proving for bit-vector programs.
• Z3/ManySat
  During two internships at Microsoft Research, I worked on the Z3 SMT solver, incorporating ideas from the ManySat project.

Publications

Books

Armin Biere, Daniel Kroening, Georg Weissenbacher, Christoph M. Wintersteiger: Digitaltechnik - eine praxisnahe Einführung Springer Verlag Berlin Heidelberg, March 2008. ISBN 978-3-540-77728-1 [BIBTEX] [LINK] [Amazon] [Springer]

Martin Helfert, Petra Mazuran, Christoph M. Wintersteiger: Gustav Tauschek und seine Maschinen Volume 10 of Geschichte der Naturwissenschaften und der Technik. Ed.: Franz Pichler, Johannes Kepler University of Linz, Austria Verlag Rudolf Trauner, Austria, February 2007. ISBN 978-3-85499-062-8 [BIBTEX] [LINK] [Amazon] [Trauner]

Peer-Reviewed Papers

Josh Berdine, Arlen Cox, Samin Ishtiaq, Christoph M. Wintersteiger:
Diagnosing Abstraction Failure for Separation Logic-based Analyses
Proceedings of CAV 2012, to appear, 2012.
[BIBTEX] [LINK] [Preprint PDF]

Youssef Hamadi, Joao Marques-Silva, Christoph M. Wintersteiger:
Lazy Decomposition for Distributed Decision Procedures
Proceedings of PDMC 2011, EPTCS, 2011.
[BIBTEX] [LINK] [Preprint PDF]

Aliaksei Tsitovich, Natasha Sharygina, Christoph M. Wintersteiger, Daniel Kroening:
Loop Summarization and Termination Analysis
Proceedings of TACAS 2011, LNCS 6605, Springer, 2011.
[BIBTEX] [LINK] [Preprint PDF]

Christoph M. Wintersteiger, Youssef Hamadi, Leonardo de Moura:
Efficiently Solving Quantified Bit-Vector Formulas
Proceedings of FMCAD 2010, IEEE, 2010.
[BIBTEX] [LINK] [Preprint PDF]

Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger:
Loopfrog -- Loop Summarization for Static Analysis
Proceedings of WING 2010, to appear, 2010.
[BIBTEX] [LINK] [Preprint PDF]

Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, Christoph M. Wintersteiger:
Termination Analysis With Compositional Transition Invariants
Proceedings of CAV 2010, LNCS 6174, Springer, 2010.
[BIBTEX] [LINK] [Preprint PDF]

Byron Cook, Daniel Kroening, Philipp Rümmer, Christoph M. Wintersteiger:
Ranking Function Synthesis for Bit-Vector Relations
Proceedings of TACAS 2010, LNCS 6015, Springer, 2010.
[BIBTEX] [LINK] [Preprint PDF]

Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger:
Loopfrog: A Static Analyzer for ANSI-C Programs
Proceedings of ASE 2009, IEEE Press, 2009.
[BIBTEX] [LINK] [Preprint PDF]

Christoph M. Wintersteiger, Youssef Hamadi, Leonardo de Moura:
A Concurrent Portfolio Approach to SMT Solving
Proceedings of CAV 2009, LNCS 5643, Springer, 2009.
[BIBTEX] [LINK] [Preprint PDF]

Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger:
Loop Summarization using Abstract Transformers
Proceedings of ATVA 2008, LNCS 5311, Springer, 2008.
[BIBTEX] [LINK] [Preprint PDF]

Toni Jussila, Armin Biere, Carsten Sinz, Daniel Kroening, Christoph M. Wintersteiger:
A First Step Towards a Unified Proof Checker for QBF
Proceedings of SAT 2007, LNCS 4501, Springer, 2007.
[BIBTEX] [LINK] [Preprint PDF]

Martin Helfert, Christoph M. Wintersteiger:
Gustav Tauschek's Punchcard Accounting Machines
Proceedings of MEDICHI2007, OCG 220, Austrian Computer Society, 2007.
[BIBTEX] [LINK] [Preprint PDF]

Theses

Christoph M. Wintersteiger:
Termination Analysis for Bit-Vector Programs
PhD Thesis (Dissertation), ETH Zurich, Switzerland, 2011.
[BIBTEX] [LINK] [PDF]

Christoph M. Wintersteiger:
Crane - Eine Kryptanalyse-Umgebung
Masters Thesis (Diplomarbeit), University of Linz, Austria, 2006.
[BIBTEX] [LINK] [PDF]

Teaching Activities

ETH Zurich

2009 Summer	252-0014-00U	Digitaltechnik (Exercises)
2008 Summer	252-0014-00U	Digitaltechnik (Exercises)
2007 Fall	251-0276-00L	Seminar on Software Engineering
2007 Fall	251-0207-00L	Seminar on Digital Design
2007 Summer	252-0014-00U	Digitaltechnik (Exercises)
2007 Summer	251-0276-00L	Seminar on Software Engineering
2006 Winter	401-0131-00U	Lineare Algebra (Exercises)
2006 Winter	251-0211-00L	Seminar on Software Engineering
2006 Winter	251-0207-00L	Seminar on Digital Design
2006 Summer	252-0014-00U	Digitaltechnik (Exercises)

Contact