Gereon Kremer

Publication Activity (10 Years)

Years Active: 2014-2023
Publications (10 Years): 28

Top Topics

Arithmetic Constraints

Satisfiability Modulo Theories

Top Venues

SC-square@SIAM AG

Publications

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
Generating and Exploiting Automated Reasoning Proof Certificates. Commun. ACM 66 (10) (2023)
Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett
Satisfiability Modulo Finite Fields. CAV (2) (2023)
Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett
Satisfiability Modulo Finite Fields. IACR Cryptol. ePrint Arch. 2023 (2023)
Gereon Kremer, Jasper Nalbach
Cylindrical Algebraic Coverings for Quantifiers (short paper). SC-Square@FLoC (2022)
Gereon Kremer, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description). IJCAR (2022)
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
cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS (1) (2022)
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
Flexible Proof Production in an Industrial-Strength SMT Solver. IJCAR (2022)
Gereon Kremer, Aina Niemetz, Mathias Preiner
ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends. CAV (2) (2021)
Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer
Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic. CoRR (2021)
Jasper Nalbach, Erika Ábrahám, Gereon Kremer
Extending the Fundamental Theorem of Linear Programming for Strict Inequalities. ISSAC (2021)
Gereon Kremer, Erika Ábrahám, Matthew England, James H. Davenport
On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving. SYNASC (2021)
Gereon Kremer, Jens Brandt
Implementing arithmetic over algebraic numbers A tutorial for Lazard's lifting scheme in CAD. SYNASC (2021)
Gereon Kremer, Erika Ábrahám, Vijay Ganesh
On the proof complexity of MCSAT. CoRR (2021)
Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer
Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings. J. Log. Algebraic Methods Program. 119 (2021)
Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer
Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic. ARCADE@CADE (2021)
Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer, Zak Tonks
New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract). PAAR+SC²@IJCAR (2020)
Gereon Kremer, Erika Ábrahám
Fully incremental cylindrical algebraic decomposition. J. Symb. Comput. 100 (2020)
Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer
Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings. CoRR (2020)
Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer, Zak Tonks
New Opportunities for the Formal Proof of Computational Real Geometry? CoRR (2020)
Gereon Kremer, Erika Ábrahám, Vijay Ganesh
On the Proof Complexity of MCSAT. SC-square@SIAM AG (2019)
Jasper Nalbach, Gereon Kremer, Erika Ábrahám
On Variable Orderings in MCSAT for Non-Linear Real Arithmetic. SC-square@SIAM AG (2019)
Rebecca Haehn, Gereon Kremer, Erika Ábrahám
Evaluation of Equational Constraints for CAD in SMT Solving. SC-Square@FLOC (2018)
Erika Ábrahám, Gereon Kremer
SMT Solving for Arithmetic Theories: Theory and Tool Support. SYNASC (2017)
Tarik Viehmann, Gereon Kremer, Erika Ábrahám
Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving. SC²@ISSAC (2017)
Erika Ábrahám, Jasper Nalbach, Gereon Kremer
Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework. SC²@ISSAC (2017)
Erika Ábrahám, Florian Corzilius, Einar Broch Johnsen, Gereon Kremer, Jacopo Mauro
Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies. SETTA (2016)
Gereon Kremer, Florian Corzilius, Erika Ábrahám
A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic. CASC (2016)
Erika Ábrahám, Gereon Kremer
Satisfiability Checking: Theory and Applications. SEFM (2016)
Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp, Erika Ábrahám
SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving. SAT (2015)
Gereon Kremer
Using Cylindrical Algebraic Decomposition in Satisfiability Modulo Theories. Joint Workshop of the German Research Training Groups in Computer Science (2014)