Using Cylindrical Algebraic Decomposition in Satisfiability Modulo Theories. - Gereon Kremer (Joint Workshop of the German Research Training Groups in Computer Science, 2014)

SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving. - Florian Corzilius; Gereon Kremer; Sebastian Junges; Stefan Schupp; Erika Ábrahám (SAT, 2015)

A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic. - Gereon Kremer; Florian Corzilius; Erika Ábrahám (CASC, 2016)

Satisfiability Checking: Theory and Applications. - Erika Ábrahám; Gereon Kremer (SEFM, 2016)

Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies. - Erika Ábrahám; Florian Corzilius; Einar Broch Johnsen; Gereon Kremer; Jacopo Mauro (SETTA, 2016)

Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework. - Erika Ábrahám; Jasper Nalbach; Gereon Kremer (SC²@ISSAC, 2017)

Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving. - Tarik Viehmann; Gereon Kremer; Erika Ábrahám (SC²@ISSAC, 2017)

SMT Solving for Arithmetic Theories: Theory and Tool Support. - Erika Ábrahám; Gereon Kremer (SYNASC, 2017)

Evaluation of Equational Constraints for CAD in SMT Solving. - Rebecca Haehn; Gereon Kremer; Erika Ábrahám (SC-Square@FLOC, 2018)

On the Proof Complexity of MCSAT. - Gereon Kremer; Erika Ábrahám; Vijay Ganesh 001 (SC-square@SIAM AG, 2019)

On Variable Orderings in MCSAT for Non-Linear Real Arithmetic. - Jasper Nalbach; Gereon Kremer; Erika Ábrahám (SC-square@SIAM AG, 2019)

New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract). - Erika Ábrahám; James H. Davenport; Matthew England 001; Gereon Kremer; Zak Tonks (PAAR+SC²@IJCAR, 2020)

New Opportunities for the Formal Proof of Computational Real Geometry? - Erika Ábrahám; James H. Davenport; Matthew England 001; Gereon Kremer; Zak Tonks (CoRR, 2020)

Fully incremental cylindrical algebraic decomposition. - Gereon Kremer; Erika Ábrahám (J. Symb. Comput., 2020)

Cylindrical algebraic decomposition for nonlinear arithmetic problems. - Gereon Kremer (2020)

Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic. - Erika Ábrahám; James H. Davenport; Matthew England 001; Gereon Kremer (ARCADE@CADE, 2021)

ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends. - Gereon Kremer; Aina Niemetz; Mathias Preiner (CAV (2), 2021)

Extending the Fundamental Theorem of Linear Programming for Strict Inequalities. - Jasper Nalbach; Erika Ábrahám; Gereon Kremer (ISSAC, 2021)

On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving. - Gereon Kremer; Erika Ábrahám; Matthew England 001; James H. Davenport (SYNASC, 2021)

Implementing arithmetic over algebraic numbers A tutorial for Lazard's lifting scheme in CAD. - Gereon Kremer; Jens Brandt 003 (SYNASC, 2021)

Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings. - Erika Ábrahám; James H. Davenport; Matthew England 001; Gereon Kremer (J. Log. Algebraic Methods Program., 2021)

Flexible Proof Production in an Industrial-Strength SMT Solver. - Haniel Barbosa; Andrew Reynolds 001; Gereon Kremer; Hanna Lachnitt; Aina Niemetz; Andres Nötzli; Alex Ozdemir; Mathias Preiner; Arjun Viswanathan 001; Scott Viteri; Yoni Zohar; Cesare Tinelli; et al. (IJCAR, 2022)

Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description). - Gereon Kremer; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (IJCAR, 2022)

Cylindrical Algebraic Coverings for Quantifiers (short paper). - Gereon Kremer; Jasper Nalbach (SC-Square@FLoC, 2022)

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 Nötzli; Alex Ozdemir; Mathias Preiner; et al. (TACAS (1), 2022)

Satisfiability Modulo Finite Fields. - Alex Ozdemir; Gereon Kremer; Cesare Tinelli; Clark W. Barrett (IACR Cryptol. ePrint Arch., 2023)

Generating and Exploiting Automated Reasoning Proof Certificates. - Haniel Barbosa; Clark W. Barrett; Byron Cook; Bruno Dutertre; Gereon Kremer; Hanna Lachnitt; Aina Niemetz; Andres Nötzli; Alex Ozdemir; Mathias Preiner; Andrew Reynolds 001; Cesare Tinelli; et al. (Commun. ACM, 2023)

Extensions of the Cylindrical Algebraic Covering Method for Quantifiers. - Jasper Nalbach; Gereon Kremer (CoRR, 2024)