Christoph M. Wintersteiger

---

Researcher in the Programming Principles and Tools 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] [Webpage] [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] [Amazon] [Trauner]

Peer-Reviewed Papers

Kroening, Sharygina, Tonetta, Tsitovich, Wintersteiger Loop Summarization using State and Transition Invariants Formal Methods in System Design (FMSD), Springer, 2012
[BIBTEX] [LINK] [Preprint PDF]

Hamadi, Wintersteiger Seven Challenges in Parallel SAT Solving AAAI, AAAI Press, 2012
[BIBTEX] [LINK] [Preprint PDF]

Wintersteiger, Hamadi, de Moura Efficiently Solving Quantified Bit-Vector Formulas Formal Methods in System Design (FMSD), Springer, 2012
[BIBTEX] [LINK] [Preprint PDF]

Berdine, Cox, Ishtiaq, Wintersteiger Diagnosing Abstraction Failure for Separation Logic-based Analyses CAV, Springer, 2012
[BIBTEX] [LINK] [Preprint PDF]

Hamadi, Marques-Silva, Wintersteiger Lazy Decomposition for Distributed Decision Procedures PDMC, EPTCS, 2011
[BIBTEX] [LINK] [Preprint PDF]

Tsitovich, Sharygina, Wintersteiger, Kroening Loop Summarization and Termination Analysis TACAS, LNCS 6605, Springer, 2011
[BIBTEX] [LINK] [Preprint PDF]

Wintersteiger, Hamadi, de Moura Efficiently Solving Quantified Bit-Vector Formulas FMCAD, IEEE, 2010
[BIBTEX] [LINK] [Preprint PDF]

Kroening, Sharygina, Tonetta, Tsitovich, Wintersteiger Loopfrog -- Loop Summarization for Static Analysis WING, EasyChair, 2010
[BIBTEX] [LINK] [Preprint PDF]

Kroening, Sharygina, Tsitovich, Wintersteiger Termination Analysis With Compositional Transition Invariants CAV, LNCS 6174, Springer, 2010
[BIBTEX] [LINK] [Preprint PDF]

Cook, Kroening, Rümmer, Wintersteiger Ranking Function Synthesis for Bit-Vector Relations TACAS, LNCS 6015, Springer, 2010
[BIBTEX] [LINK] [Preprint PDF]

Kroening, Sharygina, Tonetta, Tsitovich, Wintersteiger Loopfrog: A Static Analyzer for ANSI-C Programs ASE, IEEE Press, 2009
[BIBTEX] [LINK] [Preprint PDF]

Wintersteiger, Hamadi, de Moura A Concurrent Portfolio Approach to SMT Solving CAV, LNCS 5643, Springer, 2009
[BIBTEX] [LINK] [Preprint PDF]

Kroening, Sharygina, Tonetta, Tsitovich, Wintersteiger Loop Summarization using Abstract Transformers ATVA, LNCS 5311, Springer, 2008
[BIBTEX] [LINK] [Preprint PDF]

Jussila, Biere, Sinz, Kroening, Wintersteiger A First Step Towards a Unified Proof Checker for QBF SAT, LNCS 4501, Springer, 2007
[BIBTEX] [LINK] [Preprint PDF]

Helfert, Wintersteiger Gustav Tauschek's Punchcard Accounting Machines MEDICHI, OCG 220, Austrian Computer Society, 2007
[BIBTEX] [LINK] [Preprint PDF]

Theses

Christoph M. Wintersteiger Termination Analysis for Bit-Vector Programs Doctoral 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]

Contact