Christoph M. Wintersteiger

Researcher in the Programming Principles and Tools Group at Microsoft Research.

Current Projects


  • 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

Yordanov, Wintersteiger, Hamadi, Philipps, Kugler Functional Analysis of Large-scale DNA Strand Displacement Circuits DNA 19, LNCS, Springer, 2013
[BIBTEX] [LINK] [Preprint PDF]

Yordanov, Wintersteiger, Hamadi, Kugler SMT-based Analysis of Biological Computation NASA Formal Methods Symposium, LNCS 7871, Springer, 2013
[BIBTEX] [LINK] [Preprint PDF]

Hamadi, Wintersteiger Seven Challenges in Parallel SAT Solving AI Magazine 34:2, AAAI Press, 2013
[BIBTEX] [LINK] [Preprint PDF]

Cook, Kroening, Rümmer Wintersteiger Ranking Function Synthesis for Bit-vector Relations Formal Methods in System Design (FMSD) 43:1, Springer, 2013
[BIBTEX] [LINK] [Preprint PDF]

Kroening, Sharygina, Tonetta, Tsitovich, Wintersteiger Loop Summarization using State and Transition Invariants Formal Methods in System Design (FMSD) 42:3, Springer, 2013
[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, LNCS 7358, 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


Work Address:

Christoph M. Wintersteiger

Microsoft Research

  

21 Station Road

Cambridge, CB1 2FB

United Kingdom

  
Conferences