Gereon Kremer

According to our database, Gereon Kremer authored at least 27 papers between 2014 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

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, Cesare Tinelli, Yoni Zohar

Commun. ACM, October, 2023

Satisfiability Modulo Finite Fields.

Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett

IACR Cryptol. ePrint Arch., 2023

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, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Cylindrical Algebraic Coverings for Quantifiers (short paper).

Gereon Kremer, Jasper Nalbach

Proceedings of the 7th SC-Square Workshop co-located with the Federated Logic Conference, 2022

Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description).

Gereon Kremer, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

Flexible Proof Production in an Industrial-Strength SMT Solver.

Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark W. Barrett

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

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, Gereon Kremer

J. Log. Algebraic Methods Program., 2021

Implementing arithmetic over algebraic numbers A tutorial for Lazard's lifting scheme in CAD.

Gereon Kremer, Jens Brandt

Proceedings of the 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2021

On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving.

Gereon Kremer, Erika Ábrahám, Matthew England, James H. Davenport

Proceedings of the 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2021

Extending the Fundamental Theorem of Linear Programming for Strict Inequalities.

Jasper Nalbach, Erika Ábrahám, Gereon Kremer

Proceedings of the ISSAC '21: International Symposium on Symbolic and Algebraic Computation, 2021

ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends.

Gereon Kremer, Aina Niemetz, Mathias Preiner

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic.

Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer

Proceedings of the Third International Workshop on Automated Reasoning: Challenges, 2021

2020

Cylindrical algebraic decomposition for nonlinear arithmetic problems.

Gereon Kremer

PhD thesis, 2020

Fully incremental cylindrical algebraic decomposition.

Gereon Kremer, Erika Ábrahám

J. Symb. Comput., 2020

New Opportunities for the Formal Proof of Computational Real Geometry?

Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer, Zak Tonks

CoRR, 2020

New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract).

Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer, Zak Tonks

Proceedings of the Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020

2019

On Variable Orderings in MCSAT for Non-Linear Real Arithmetic.

Jasper Nalbach, Gereon Kremer, Erika Ábrahám

Proceedings of the 4th SC-Square Workshop co-located with the SIAM Conference on Applied Algebraic Geometry, 2019

On the Proof Complexity of MCSAT.

Gereon Kremer, Erika Ábrahám, Vijay Ganesh

Proceedings of the 4th SC-Square Workshop co-located with the SIAM Conference on Applied Algebraic Geometry, 2019

2018

Evaluation of Equational Constraints for CAD in SMT Solving.

Rebecca Haehn, Gereon Kremer, Erika Ábrahám

Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation co-located with Federated Logic Conference, 2018

2017

SMT Solving for Arithmetic Theories: Theory and Tool Support.

Erika Ábrahám, Gereon Kremer

Proceedings of the 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2017

Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving.

Tarik Viehmann, Gereon Kremer, Erika Ábrahám

Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation co-located with the 42nd International Symposium on Symbolic and Algebraic Computation (ISSAC 2017), 2017

Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework.

Erika Ábrahám, Jasper Nalbach, Gereon Kremer

Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation co-located with the 42nd International Symposium on Symbolic and Algebraic Computation (ISSAC 2017), 2017

2016

Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies.

Erika Ábrahám, Florian Corzilius, Einar Broch Johnsen, Gereon Kremer, Jacopo Mauro

Proceedings of the Dependable Software Engineering: Theories, Tools, and Applications, 2016

Satisfiability Checking: Theory and Applications.

Erika Ábrahám, Gereon Kremer

Proceedings of the Software Engineering and Formal Methods - 14th International Conference, 2016

A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic.

Gereon Kremer, Florian Corzilius, Erika Ábrahám

Proceedings of the Computer Algebra in Scientific Computing - 18th International Workshop, 2016

2015

SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving.

Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp, Erika Ábrahám

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2015, 2015

2014

Using Cylindrical Algebraic Decomposition in Satisfiability Modulo Theories.

Gereon Kremer

Proceedings of the 8th Joint Workshop of the German Research Training Groups in Computer Science, 2014