Gereon Kremer

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