CM Wintersteiger

Christoph M. Wintersteiger

Senior Research Software Development Engineer at Microsoft Research.

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.
  • ManySat
    During two internships at Microsoft Research, I worked on the Z3 SMT solver, incorporating ideas from the ManySat project.
  • The Z3 Theorem Prover and SMT Solver
    I work on finite-domain decision procedures. Sound, complete and efficient.
  • DeSAT (Paper/Code)
    Parallel and distributed SAT solvers that aim to solve bigger problems faster.

Publications (see also DBLP)


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
[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
[Amazon] [Trauner]


Peer-Reviewed Papers

Zeljić, Wintersteiger, Rümmer An Approximation Framework for Solvers and Decision Procedures JAR, Springer, 2016
[LINK] [SharedIt] [Preprint PDF]

Shavit, Yordanov, Dunn, Wintersteiger, Otani, Hamadi, Livesey, Kugler Automated Synthesis and Analysis of Switching Gene Regulatory Networks Biosystems 146, Elsevier, 2016
[LINK] [Preprint PDF]

Backeman, Dunn, Yordanov, Wintersteiger Algebraic Polynomial-based Synthesis for Abstract Boolean Network Analysis SMT, CEUR-WS 1617, 2016
[LINK] [Preprint PDF]

Janota, Wintersteiger On Intervals and Bounds in Bit-vector Arithmetic SMT, CEUR-WS 1617, 2016
[LINK] [Preprint PDF]

Zeljić, Wintersteiger, Rümmer Deciding Bit-Vector Formulas with mcSAT SAT, LNCS 9710, Springer, 2016
[LINK] [Preprint PDF]

Shavit, Yordanov, Dunn, Wintersteiger, Hamadi, Kugler Switching Gene Regulatory Networks IPCAT, LNCS 9303, Springer, 2015
[LINK] [Preprint PDF]

Fröhlich, Biere, Wintersteiger, Hamadi Stochastic Local Search for Satisfiability Modulo Theories AAAI, AAAI Press, 2015
[LINK] [Preprint PDF]

Rabe, Wintersteiger, Kugler, Yordanov, Hamadi Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains QEST, LNCS 8657, Springer, 2014
[LINK] [Preprint PDF]

Zeljić, Wintersteiger, Rümmer Approximations for Model Construction IJCAR, LNAI 8562, Springer, 2014
Received the IJCAR 2014 best paper award!
[LINK] [Preprint PDF]

Paoletti, Yordanov, Hamadi, Wintersteiger, Kugler Analyzing and Synthesizing Genomic Logic Functions CAV, LNCS 8559, Springer, 2014
[LINK] [Preprint PDF]

Berdine, Bjørner, Ishtiaq, Kriener, Wintersteiger Resourceful Reachability as HORN-LA LPAR, LNCS 8312, Springer, 2013
[LINK] [Preprint PDF]

Yordanov, Wintersteiger, Hamadi, Kugler Z34Bio: An SMT-based Framework for Analyzing Biological Computation SMT, 2013
[LINK] [Preprint PDF]

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

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

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

Wintersteiger, Hamadi, de Moura Efficiently Solving Quantified Bit-Vector Formulas Formal Methods in System Design (FMSD), Springer, 2013
[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
[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
[LINK] [Preprint PDF]

Hamadi, Wintersteiger Seven Challenges in Parallel SAT Solving AAAI, AAAI Press, 2012
[LINK] [Preprint PDF]

Berdine, Cox, Ishtiaq, Wintersteiger Diagnosing Abstraction Failure for Separation Logic-based Analyses CAV, LNCS 7358, Springer, 2012
[LINK] [Preprint PDF]

Hamadi, Marques-Silva, Wintersteiger Lazy Decomposition for Distributed Decision Procedures PDMC, EPTCS, 2011
[LINK] [Preprint PDF]

Tsitovich, Sharygina, Wintersteiger, Kroening Loop Summarization and Termination Analysis TACAS, LNCS 6605, Springer, 2011
[LINK] [Preprint PDF]

Wintersteiger, Hamadi, de Moura Efficiently Solving Quantified Bit-Vector Formulas FMCAD, IEEE, 2010
[LINK] [Preprint PDF]

Kroening, Sharygina, Tonetta, Tsitovich, Wintersteiger Loopfrog -- Loop Summarization for Static Analysis WING, EasyChair, 2010
[LINK] [Preprint PDF]

Kroening, Sharygina, Tsitovich, Wintersteiger Termination Analysis With Compositional Transition Invariants CAV, LNCS 6174, Springer, 2010
[LINK] [Preprint PDF]

Cook, Kroening, Rümmer, Wintersteiger Ranking Function Synthesis for Bit-Vector Relations TACAS, LNCS 6015, Springer, 2010
[LINK] [Preprint PDF]

Kroening, Sharygina, Tonetta, Tsitovich, Wintersteiger Loopfrog: A Static Analyzer for ANSI-C Programs ASE, IEEE Press, 2009
[LINK] [Preprint PDF]

Wintersteiger, Hamadi, de Moura A Concurrent Portfolio Approach to SMT Solving CAV, LNCS 5643, Springer, 2009
[LINK] [Preprint PDF]

Kroening, Sharygina, Tonetta, Tsitovich, Wintersteiger Loop Summarization using Abstract Transformers ATVA, LNCS 5311, Springer, 2008
[LINK] [Preprint PDF]

Jussila, Biere, Sinz, Kroening, Wintersteiger A First Step Towards a Unified Proof Checker for QBF SAT, LNCS 4501, Springer, 2007
[LINK] [Preprint PDF]

Helfert, Wintersteiger Gustav Tauschek's Punchcard Accounting Machines MEDICHI, OCG 220, Austrian Computer Society, 2007
[LINK] [Preprint PDF]


Theses

Christoph M. Wintersteiger Termination Analysis for Bit-Vector Programs Doctoral Thesis (Dissertation), ETH Zurich, Switzerland, 2011
[LINK] [PDF]

Christoph M. Wintersteiger Crane - Eine Kryptanalyse-Umgebung Masters Thesis (Diplomarbeit), University of Linz, Austria, 2006
[LINK] [PDF]

 

 

Contact

Work Address:

Christoph M. Wintersteiger

Microsoft Research

  

21 Station Road

Cambridge, CB1 2FB

United Kingdom
  
Conferences