A First Step Towards a Unified Proof Checker for QBF. - Toni Jussila; Armin Biere; Carsten Sinz; Daniel Kröning; Christoph M. Wintersteiger (SAT, 2007)

Loop Summarization Using Abstract Transformers. - Daniel Kroening; Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich; Christoph M. Wintersteiger (ATVA, 2008)

A Concurrent Portfolio Approach to SMT Solving. - Christoph M. Wintersteiger; Youssef Hamadi; Leonardo Mendonça de Moura (CAV, 2009)

Loopfrog: A Static Analyzer for ANSI-C Programs. - Daniel Kroening; Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich; Christoph M. Wintersteiger (ASE, 2009)

Loopfrog - loop summarization for static analysis. - Daniel Kroening; Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich; Christoph M. Wintersteiger (WING@ETAPS/IJCAR, 2010)

Termination Analysis with Compositional Transition Invariants. - Daniel Kroening; Natasha Sharygina; Aliaksei Tsitovich; Christoph M. Wintersteiger (CAV, 2010)

Loop Summarization and Termination Analysis. - Aliaksei Tsitovich; Natasha Sharygina; Christoph M. Wintersteiger; Daniel Kroening (TACAS, 2011)

Lazy Decomposition for Distributed Decision Procedures - Youssef Hamadi; João Marques-Silva 001; Christoph M. Wintersteiger (PDMC, 2011)

Termination Analysis for Bit-Vector Programs. - Christoph M. Wintersteiger (2011)

Diagnosing Abstraction Failure for Separation Logic-Based Analyses. - Josh Berdine; Arlen Cox; Samin Ishtiaq; Christoph M. Wintersteiger (CAV, 2012)

Functional Analysis of Large-Scale DNA Strand Displacement Circuits. - Boyan Yordanov; Christoph M. Wintersteiger; Youssef Hamadi; Andrew Phillips; Hillel Kugler (DNA, 2013)

Resourceful Reachability as HORN-LA. - Josh Berdine; Nikolaj S. Bjørner; Samin Ishtiaq; Jael E. Kriener; Christoph M. Wintersteiger (LPAR, 2013)

SMT-Based Analysis of Biological Computation. - Boyan Yordanov; Christoph M. Wintersteiger; Youssef Hamadi; Hillel Kugler (NASA Formal Methods, 2013)

Seven Challenges in Parallel SAT Solving. - Youssef Hamadi; Christoph M. Wintersteiger (AI Mag., 2013)

Ranking function synthesis for bit-vector relations. - Byron Cook; Daniel Kroening; Philipp Rümmer; Christoph M. Wintersteiger (Formal Methods Syst. Des., 2013)

Loop summarization using state and transition invariants. - Daniel Kroening; Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich; Christoph M. Wintersteiger (Formal Methods Syst. Des., 2013)

Efficiently solving quantified bit-vector formulas. - Christoph M. Wintersteiger; Youssef Hamadi; Leonardo Mendonça de Moura (Formal Methods Syst. Des., 2013)

Approximations for Model Construction. - Aleksandar Zeljic; Christoph M. Wintersteiger; Philipp Rümmer (IJCAR, 2014)

Analyzing and Synthesizing Genomic Logic Functions. - Nicola Paoletti; Boyan Yordanov; Youssef Hamadi; Christoph M. Wintersteiger; Hillel Kugler (CAV, 2014)

Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains. - Markus N. Rabe; Christoph M. Wintersteiger; Hillel Kugler; Boyan Yordanov; Youssef Hamadi (QEST, 2014)

Stochastic Local Search for Satisfiability Modulo Theories. - Andreas Fröhlich; Armin Biere; Christoph M. Wintersteiger; Youssef Hamadi (AAAI, 2015)

Switching Gene Regulatory Networks. - Yoli Shavit; Boyan Yordanov; Sara-Jane Dunn; Christoph M. Wintersteiger; Youssef Hamadi; Hillel Kugler (IPCAT, 2015)

Algebraic Polynomial-based Synthesis for Abstract Boolean Network Analysis. - Peter Backeman; Christoph M. Wintersteiger; Boyan Yordanov; Sara-Jane Dunn (SMT@IJCAR, 2016)

On Intervals and Bounds in Bit-vector Arithmetic. - Mikolás Janota; Christoph M. Wintersteiger (SMT@IJCAR, 2016)

Deciding Bit-Vector Formulas with mcSAT. - Aleksandar Zeljic; Christoph M. Wintersteiger; Philipp Rümmer (SAT, 2016)

Automated Synthesis and Analysis of Switching Gene Regulatory Networks. - Yoli Shavit; Boyan Yordanov; Sara-Jane Dunn; Christoph M. Wintersteiger; Tomoki Otani; Youssef Hamadi; Frederick J. Livesey; Hillel Kugler (Biosyst., 2016)

Relating Complexity-theoretic Parameters with SAT Solver Performance. - Edward Zulkoski; Ruben Martins; Christoph M. Wintersteiger; Robert Robere; Jia Liang; Krzysztof Czarnecki 001; Vijay Ganesh 001 (CoRR, 2017)

An Approximation Framework for Solvers and Decision Procedures. - Aleksandar Zeljic; Christoph M. Wintersteiger; Philipp Rümmer (J. Autom. Reason., 2017)

Parallel Satisfiability Modulo Theories. - Antti E. J. Hyvärinen; Christoph M. Wintersteiger (Handbook of Parallel Constraint Reasoning, 2018)

Exploring Approximations for Floating-Point Arithmetic Using UppSAT. - Aleksandar Zeljic; Peter Backeman; Christoph M. Wintersteiger; Philipp Rümmer (IJCAR, 2018)

The Effect of Structural Measures and Merges on SAT Solver Performance. - Edward Zulkoski; Ruben Martins; Christoph M. Wintersteiger; Jia Hui Liang; Krzysztof Czarnecki 001; Vijay Ganesh 001 (CP, 2018)

Learning-Sensitive Backdoors with Restarts. - Edward Zulkoski; Ruben Martins; Christoph M. Wintersteiger; Robert Robere; Jia Hui Liang; Krzysztof Czarnecki 001; Vijay Ganesh 001 (CP, 2018)

Programming Z3. - Nikolaj S. Bjørner; Leonardo de Moura 001; Lev Nachmanson; Christoph M. Wintersteiger (SETSS, 2018)

Compositional Taylor Model Based Validated Integration. - Kristjan Liiva; Paul B. Jackson; Grant O. Passmore; Christoph M. Wintersteiger (SYNASC, 2018)

SCNS: a graphical tool for reconstructing executable regulatory networks from single-cell genomic data. - Steven Woodhouse; Nir Piterman; Christoph M. Wintersteiger; Berthold Göttgens; Jasmin Fisher (BMC Syst. Biol., 2018)

Large-scale Genetic Exploration of Genome-wide Models: an Application to Human Cancer Metabolism. - Youssef Hamadi; Claudio Angione; Hillel Kugler; Christoph M. Wintersteiger; Boyan Yordanov (IEEE DataPort, 2018)

snmalloc: a message passing allocator. - Paul Liétar; Theodore Butler; Sylvan Clebsch; Sophia Drossopoulou; Juliana Franco; Matthew J. Parkinson; Alex Shamis; Christoph M. Wintersteiger; David Chisnall (ISMM, 2019)

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. - Jonathan Protzenko; Bryan Parno; Aymeric Fromherz; Chris Hawblitzel; Marina Polubelova; Karthikeyan Bhargavan; Benjamin Beurdouche; Joonwon Choi; Antoine Delignat-Lavaud; Cédric Fournet; Tahina Ramananandro; Aseem Rastogi; et al. (IACR Cryptol. ePrint Arch., 2019)

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. - Jonathan Protzenko; Bryan Parno; Aymeric Fromherz; Chris Hawblitzel; Marina Polubelova; Karthikeyan Bhargavan; Benjamin Beurdouche; Joonwon Choi; Antoine Delignat-Lavaud; Cédric Fournet; Natalia Kulatova; Tahina Ramananandro; et al. (SP, 2020)

Discovering Essential Multiple Gene Effects Through Large Scale Optimization: An Application to Human Cancer Metabolism. - Annalisa Occhipinti; Youssef Hamadi; Hillel Kugler; Christoph M. Wintersteiger; Boyan Yordanov; Claudio Angione (IEEE ACM Trans. Comput. Biol. Bioinform., 2021)

An SMT-Based Framework for Reasoning About Discrete Biological Models. - Boyan Yordanov; Sara-Jane Dunn; Colin Gravill; Hillel Kugler; Christoph M. Wintersteiger (ISBRA, 2022)

IA-CCF: Individual Accountability for Permissioned Ledgers. - Alex Shamis; Peter R. Pietzuch; Burcu Canakci; Miguel Castro 001; Cédric Fournet; Edward Ashton; Amaury Chamayou; Sylvan Clebsch; Antoine Delignat-Lavaud; Matthew Kerner; Julien Maffre; Olga Vrousgou; et al. (NSDI, 2022)

COCOAEXPO: Confidential Containers via Attested Execution Policies. - Matthew A. Johnson 003; Stavros Volos; Ken Gordon; Sean T. Allen; Christoph M. Wintersteiger; Sylvan Clebsch; John Starks; Manuel Costa (CoRR, 2023)

Confidential Consortium Framework: Secure Multiparty Applications with Confidentiality, Integrity, and High Availability. - Heidi Howard; Fritz Alder; Edward Ashton; Amaury Chamayou; Sylvan Clebsch; Manuel Costa; Antoine Delignat-Lavaud; Cédric Fournet; Andrew Jeffery; Matthew Kerner; Fotios Kounelis; Markus A. Kuppe; et al. (Proc. VLDB Endow., 2023)

The Reasoning Engine: A Satisfiability Modulo Theories-Based Framework for Reasoning About Discrete Biological Models. - Boyan Yordanov; Sara-Jane Dunn; Colin Gravill; Himanshu Arora; Hillel Kugler; Christoph M. Wintersteiger (J. Comput. Biol., 2023)

Confidential Container Groups: Implementing confidential computing on Azure container instances. - Matthew A. Johnson 003; Stavros Volos; Ken Gordon; Sean T. Allen; Christoph M. Wintersteiger; Sylvan Clebsch; John Starks; Manuel Costa (ACM Queue, 2024)

Confidential Container Groups. - Matthew A. Johnson 003; Stavros Volos; Ken Gordon; Sean T. Allen; Christoph M. Wintersteiger; Sylvan Clebsch; John Starks; Manuel Costa (Commun. ACM, 2024)

Formal Verification of the IEEE P3109 Standard for Binary Floating-Point Formats for Machine Learning. - Christoph M. Wintersteiger (ARITH, 2025)

Transparent Attested DNS for Confidential Computing Services. - Antoine Delignat-Lavaud; Cédric Fournet; Kapil Vaswani; Manuel Costa; Sylvan Clebsch; Christoph M. Wintersteiger (CoRR, 2025)