Christoph M. Wintersteiger

---

Research Interests

Þ Formal Software Verification	Þ Cryptography and Cryptanalysis
Þ Heuristic and Parallel Algorithms	Þ Complexity Theory
Þ Optimization (of) Algorithms	Þ Algorithmic Number Theory
Þ Artificial Intelligence	Þ Computational Physics
Þ ... and of course all combinations of these.

Current Projects

Þ squolem/qbv
When you can't trust your QBF solver, you'll need certificates. We did a few experiments on that.

Þ SATABS/CBMC: goto-cc
We 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.

Þ 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

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

Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger:
Loopfrog -- Loop Summarization for Static Analysis (Tool Abstract)
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:
Crane - Eine Kryptanalyse-Umgebung.
Masters Thesis (Diplomarbeit), University of Linz, Austria, February 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