Gereon Kremer

Most-cited papers

cvc5: A Versatile and Industrial-Strength SMT Solver
Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer +12 more
2022International Conference on Tools and Algorithms for Construction and Analysis of Systems594 citations Open access
Semantic Scholar
SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp +1 more
2015International Conference on Theory and Applications of Satisfiability Testing101 citations
Semantic Scholar
Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings
Erika Ábrahám, J. Davenport, M. England, Gereon Kremer
2020J. Log. Algebraic Methods Program.54 citations Open access
Semantic Scholar
Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies
E. Ábrahám, Florian Corzilius, E. Johnsen, Gereon Kremer +1 more
2016International Symposium on Software Engineering: Theories, Tools, and Applications40 citations
Semantic Scholar
Flexible Proof Production in an Industrial-Strength SMT Solver
Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt +9 more
2022International Joint Conference on Automated Reasoning32 citations Open access
Semantic Scholar
Fully incremental cylindrical algebraic decomposition
Gereon Kremer, E. Ábrahám
2020Journal of symbolic computation25 citations Open access
Semantic Scholar
ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends
Gereon Kremer, Aina Niemetz, M. Preiner
2021International Conference on Computer Aided Verification24 citations Open access
Semantic Scholar
Satisfiability Modulo Finite Fields
Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett
2023IACR Cryptology ePrint Archive23 citations Open access
Semantic Scholar
Cylindrical algebraic decomposition for nonlinear arithmetic problems
Gereon Kremer
202022 citations
Semantic Scholar
Satisfiability Checking: Theory and Applications
E. Ábrahám, Gereon Kremer
2016IEEE International Conference on Software Engineering and Formal Methods19 citations
Semantic Scholar
Generating and Exploiting Automated Reasoning Proof Certificates
Haniel Barbosa, Clark W. Barrett, Byron Cook, Bruno Dutertre +9 more
2023Communications of the ACM18 citations Open access
Semantic Scholar
A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic
Gereon Kremer, Florian Corzilius, E. Ábrahám
2016Computer Algebra in Scientific Computing15 citations Open access
Semantic Scholar
Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description)
Gereon Kremer, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2022International Joint Conference on Automated Reasoning12 citations Open access
Semantic Scholar
New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract)
Erika Ábrahám, J. Davenport, M. England, Gereon Kremer +1 more
2020PAAR+SC²@IJCAI11 citations
Semantic Scholar
Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework
E. Ábrahám, Jasper Nalbach, Gereon Kremer
2017SC²@ISSAC11 citations
Semantic Scholar
SMT Solving for Arithmetic Theories: Theory and Tool Support
E. Ábrahám, Gereon Kremer
2017Symposium on Symbolic and Numeric Algorithms for Scientific Computing10 citations
Semantic Scholar
On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving
Gereon Kremer, E. Ábrahám, M. England, J. Davenport
2021Symposium on Symbolic and Numeric Algorithms for Scientific Computing9 citations Open access
Semantic Scholar
On Variable Orderings in MCSAT for Non-Linear Real Arithmetic
Jasper Nalbach, Gereon Kremer, E. Ábrahám
2019SC-square@SIAM AG9 citations
Semantic Scholar
Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving
Tarik Viehmann, Gereon Kremer, E. Ábrahám
2017SC²@ISSAC7 citations
Semantic Scholar
Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
E. Ábrahám, J. Davenport, M. England, Gereon Kremer
2021ARCADE@CADE5 citations
Semantic Scholar
Modular strategic SMT solving with SMT-RAT
Gereon Kremer, E. Ábrahám
2018Acta Universitatis Sapientiae: Informatica5 citations Open access
Semantic Scholar
Extensions of the Cylindrical Algebraic Covering Method for Quantifiers
Jasper Nalbach, Gereon Kremer
2024Mathematics and Computer Science4 citations
Semantic Scholar
Implementing arithmetic over algebraic numbers A tutorial for Lazard's lifting scheme in CAD
Gereon Kremer, J. Brandt
2021Symposium on Symbolic and Numeric Algorithms for Scientific Computing3 citations
Semantic Scholar
A novel adaption of the Simplex algorithm for linear real arithmetic
Jasper Nalbach, E. Ábrahám, C. Büsing, Gereon Kremer
20203 citations
Semantic Scholar
Isolating Real Roots Using Adaptable-Precision Interval Arithmetic
Gereon Kremer, E. Ábrahám, P. Rossmanith
20133 citations
Semantic Scholar
CVC 5 at the SMT Competition 2022
Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer +10 more
3 citations
Semantic Scholar
Extending the Fundamental Theorem of Linear Programming for Strict Inequalities
Jasper Nalbach, E. Ábrahám, Gereon Kremer
2021International Symposium on Symbolic and Algebraic Computation2 citations
Semantic Scholar
Evaluation of Equational Constraints for CAD in SMT Solving
Rebecca Haehn, Gereon Kremer, E. Ábrahám
2018SC-Square@FLOC2 citations
Semantic Scholar
Cylindrical Algebraic Coverings for Quantifiers (short paper)
Gereon Kremer, Jasper Nalbach
2022SC-Square@FLoC1 citations
Semantic Scholar
On the Proof Complexity of MCSAT
Gereon Kremer, E. Ábrahám, Vijay Ganesh
2021SC-square@SIAM AG1 citations
Semantic Scholar
USING FOURIER-MOTZKIN VARIABLE ELIMINATION FOR MCSAT EXPLANATIONS IN SMT-RAT
L. Bartolomé, Gereon Kremer
20181 citations
Semantic Scholar
CVC 5 at the SMT Competition 2021
Clark W. Barrett, Haniel Barbosa, Martin Brain, Gereon Kremer +10 more
1 citations
Semantic Scholar
INCREMENTAL CAD PROJECTION
Rebecca Haehn, Gereon Kremer
20180 citations
Semantic Scholar
SOLVING PSEUDO-BOOLEAN CONSTRAINTS
M. Grobelna, E. Ábrahám, Gereon Kremer
20170 citations
Semantic Scholar
Using Cylindrical Algebraic Decomposition in Satisfiability Modulo Theories
Gereon Kremer
2014Joint Workshop of the German Research Training Groups in Computer Science0 citations
Semantic Scholar
The Next Generation of Deduction Systems: From Composition to Compositionality
MariaPaolaBonacina, PascalFontaine, CláudiaNalon, ClaudiaSchon +46 more
0 citations
Semantic Scholar