| 2023 | CAV | Satisfiability Modulo Finite Fields. | Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett |
| 2022 | CADE | Flexible Proof Production in an Industrial-Strength SMT Solver. | Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Ntzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark W. Barrett |
| 2022 | CADE | Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description). | Gereon Kremer, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2022 | TACAS | cvc5: A Versatile and Industrial-Strength SMT Solver. | Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Ntzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar |
| 2021 | CAV | ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends. | Gereon Kremer, Aina Niemetz, Mathias Preiner |
| 2021 | ISSAC | Extending the Fundamental Theorem of Linear Programming for Strict Inequalities. | Jasper Nalbach, Erika brahm, Gereon Kremer |
| 2021 | SYNASC | On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving. | Gereon Kremer, Erika brahm, Matthew England, James H. Davenport |
| 2021 | SYNASC | Implementing arithmetic over algebraic numbers A tutorial for Lazard's lifting scheme in CAD. | Gereon Kremer, Jens Brandt |
| 2020 | CADE | New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract). | Erika brahm, James H. Davenport, Matthew England, Gereon Kremer, Zak Tonks |
| 2017 | ISSAC | Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework. | Erika brahm, Jasper Nalbach, Gereon Kremer |
| 2017 | ISSAC | Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving. | Tarik Viehmann, Gereon Kremer, Erika brahm |
| 2017 | SYNASC | SMT Solving for Arithmetic Theories: Theory and Tool Support. | Erika brahm, Gereon Kremer |
| 2016 | CASC | A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic. | Gereon Kremer, Florian Corzilius, Erika brahm |
| 2016 | SEFM | Satisfiability Checking: Theory and Applications. | Erika brahm, Gereon Kremer |
| 2016 | SETTA | Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies. | Erika brahm, Florian Corzilius, Einar Broch Johnsen, Gereon Kremer, Jacopo Mauro |
| 2015 | SAT | SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving. | Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp, Erika brahm |