Christoph M. Wintersteiger

Christoph M. Wintersteiger
RESEARCHER
.

I'm a researcher in the Programming Principles and Tools Group, working on SAT solvers with the Constraint Reasoning Group and SMT solvers, e.g., the Z3 theorem prover

Together with Aleksandar Zeljić and Philipp Rümmer, I received the IJCAR 2014 best paper award for our paper on Approximations for Model Construction!

Projects
  • Z3: Theorem Prover
    Z3 is a high-performance theorem prover being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools from Microsoft Research.
  • Z3-4Biology
    SMT-based Analysis of Biological Computation
  • Declarative Problem Solving
    What is the link between how problems are logically described in a formal language, and how they are solved by algorithms?
Downloads
Publications

2014

Markus N. Rabe, Christoph M. Wintersteiger, Hillel Kugler, Boyan Yordanov, and Youssef Hamadi, Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains, Springer, September 2014

Aleksandar Zeljic, Christoph M. Wintersteiger, and Philipp Rummer, Approximations for Model Construction, in Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR 2014), Springer, July 2014

Nicola Paoletti, Boyan Yordanov, Youssef Hamadi, Christoph M. Wintersteiger, and Hillel Kugler, Analyzing and Synthesizing Genomic Logic Functions, in CAV'14, Springer, July 2014

Markus N. Rabe, Christoph M. Wintersteiger, Hillel Kugler, Boyan Yordanov, and Youssef Hamadi, Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains (Extended), no. MSR-TR-2014-74, 23 May 2014

2013

Josh Berdine, Nikolaj Bjørner, Samin Ishtiaq, Jael E. Kriener, and Christoph M. Wintersteiger, Resourceful Reachability as HORN-LA, in International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Springer, 15 December 2013

Boyan Yordanov, Christoph Wintersteiger, Youssef Hamadi, Andrew Phillips, and Hillel Kugler, Functional Analysis of Large-scale DNA Strand Displacement Circuits, in International Conference on DNA Computing and Molecular Programming, vol. 8141, pp. 189-203, Springer, September 2013

Boyan Yordanov, Christoph M. Wintersteiger, Youssef Hamadi, and Hillel Kugler, Z34Bio: An SMT-based Framework for Analyzing Biological Computation, in SMT'13, July 2013

Boyan Yordanov, Christoph M. Wintersteiger, Youssef Hamadi, and Hillel Kugler, SMT-based Analysis of Biological Computation, in NASA Formal Methods Symposium 2013, Springer Verlag, May 2013

Byron Cook, Daniel Kroening, Philipp Rümmer, and Christoph M. Wintersteiger, Ranking function synthesis for bit-vector relations, in Formal Methods in System Design, vol. 43, no. 1, pp. 93-120 , 2013

Youssef Hamadi and Christoph M. Wintersteiger, Seven Challenges in Parallel SAT Solving, in AI Magazine, vol. 34, no. 2, pp. 99-106, AAAI, 2013

Christoph M. Wintersteiger, Youssef Hamadi, and Leonardo de Moura, Efficiently Solving Quantified Bit-Vector Formulas, in Formal Methods in System Design, vol. 42, no. 1, pp. 3-23, Springer, 2013

Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, and Christoph M. Wintersteiger, Loop summarization using state and transition invariants, in Formal Methods in System Design, vol. 42, no. 3, pp. 221-261, Springer, 2013

2012

Josh Berdine, Arlen Cox, Samin Ishtiaq, and Christoph M. Wintersteiger, Diagnosing Abstraction Failure for Separation Logic-based Analyses, in Proceedings of the 24th International Conference on Computer Aided Verification (CAV), Springer, July 2012

Antti E. J. Hyvarinen and Christoph M. Wintersteiger, Approaches for Multi-Core Propagation in Clause Learning Satisfiability Solvers, no. MSR-TR-2012-47, 1 May 2012

Josh Berdine, Arlen Cox, Samin Ishtiaq, and Christoph M. Wintersteiger, Diagnosing Abstraction Failure for Separation Logic-based Analyses, no. MSR-TR-2012-44, April 2012

Boyan Yordanov, Christoph M. Wintersteiger, Youssef Hamadi, and Hillel Kugler, Z3-4biology SMT-based analysis of biological computation, no. MSR-TR-2012-31, 12 March 2012

Youssef Hamadi and Christoph M. Wintersteiger, Seven Challenges in Parallel SAT Solving, in Proceedings of AAAI-12, American Association for Artificial Intelligence , 2012

2011

Aliaksei Tsitovich, Natasha Sharygina, Christoph M. Wintersteiger, and Daniel Kroening, Loop Summarization and Termination Analysis, in Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Springer Verlag, 2011

Youssef Hamadi, Joao Marques-Silva, and Christoph M. Wintersteiger, Lazy Decomposition for Distributed Decision Procedures, in Proceedings of the 10th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC'11), Electronic Proceedings in Theoretical Computer Science, 2011

2010

Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, and Christoph M. Wintersteiger, Termination Analysis With Compositional Transition Invariants, in Proceedings of the 22nd International Conference on Computer Aided Verification (CAV), Springer, 2010

Christoph M. Wintersteiger, Youssef Hamadi, and Leonardo de Moura, Efficiently Solving Quantified Bit-Vector Formulas, in Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD), 2010

Byron Cook, Daniel Kroening, Philipp Rümmer, and Christoph M. Wintersteiger, Ranking Function Synthesis for Bit-Vector Relations, in Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Springer, 2010

2009

Christoph M. Wintersteiger, Youssef Hamadi, and Leonardo de Moura, A Concurrent Portfolio Approach to SMT Solving, in Proceedings of the 21st International Conference on Computer Aided Verification (CAV), Springer, 2009

Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, and Christoph M. Wintersteiger, Loopfrog: A Static Analyzer for ANSI-C Programs, in Proceedings of ASE 2009, IEEE Press, 2009

2008

Armin Biere, Daniel Kroening, Georg Weissenbacher, and Christoph M. Wintersteiger, Digitaltechnik - eine praxisnahe Einführung, Springer Verlag Berlin Heidelberg, 2008

Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, and Christoph M. Wintersteiger, Loop Summarization using Abstract Transformers, in Proceedings of ATVA 2008, Springer, 2008

2007

Martin Helfert and Christoph M. Wintersteiger, Gustav Tauschek's Punchcard Accounting Machines, in MEDICHI 2007 - Methodic and Didactic Challenges of the History of Informatics, Austrian Computer Society, 2007

Toni Jussila, Armin Biere, Carsten Sinz, Daniel Kroening, and Christoph M. Wintersteiger, A First Step Towards a Unified Proof Checker for QBF, in Proceedings of the Tenth International Conference on Theory and Applications of Satisfiability Testing (SAT 2007), Springer, 2007

Martin Helfert, Petra Mazuran, and Christoph M. Wintersteiger, Gustav Tauschek und seine Maschinen, vol. 10, Verlag Rudolf Trauner, Austria, 2007