|
Christoph M. Wintersteiger
Post-doctoral researcher in the
Constraint Reasoning 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]
[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
Contact
Work Address:
|
|
Christoph M. Wintersteiger |
Microsoft Research |
|
| | |
7 JJ Thomson Ave |
Cambridge, CB3 0FB |
United Kingdom |
| | |
|