Þ
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]