Gereon Kremer | Publications

Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark Barrett. "Satisfiability Modulo Finite Fields". In Computer Aided Verification (CAV 2023), pp. 163-186. 2023. open access 10.1007/978-3-031-37703-7_8 eprint @ iacr

Gereon Kremer, Jasper Nalbach. "Cylindrical Algebraic Coverings for Quantifiers". In Satisfiability Checking and Symbolic Computation (SC² 2022), CEUR Workshop Proceedings vol. 3458. 2022. preprint open access Vol-3458/paper1.pdf

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 Barrett. "Flexible Proof Production in an Industrial-Strength SMT Solver". In International Joint Conference on Automated Reasoning (IJCAR 2022), pp. 15-35. 2022. preprint open access 10.1007/978-3-031-10769-6_3

Gereon Kremer, Andrew Reynolds, Clark Barrett, Cesare Tinelli. "Cooperating Techniques for Solving nonlinear arithmetic in the cvc5 SMT solver (System Description)". In International Joint Conference on Automated Reasoning (IJCAR 2022), pp. 95-105. 2022. preprint open access 10.1007/978-3-031-10769-6_7

Haniel Barbosa, Clark 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". In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022), pp. 415-442. 2022. preprint open access SCP best tool paper award 10.1007/978-3-030-99524-9_24

Gereon Kremer, Erika Ábrahám, Matthew England, James H. Davenport. "On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving". In Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2021), pp. 37-39. 2021. preprint 10.1109/SYNASC54541.2021.00018

Gereon Kremer, Jens Brandt. "Implementing arithmetic over algebraic numbers: A tutorial for Lazard's lifting scheme in CAD". In Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2021), pp. 4-10. 2021. preprint 10.1109/SYNASC54541.2021.00013

Jasper Nalbach, Erika Ábrahám, Gereon Kremer. "Extending the fundamental theorem of linear programming for strict inequalities". In International Symposium on Symbolic and Algebraic Computation (ISSAC 2021), pp. 313-320. 2021. preprint 10.1145/3452143.3465538

Gereon Kremer, Aina Niemetz, Mathias Preiner. "ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends". In Computer-Aided Verification (CAV 2021), LNCS vol. 12760, pp. 231-242. 2021. preprint open access 10.1007/978-3-030-81688-9_11 artifact: 4721925

Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer. "Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic". In Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2021). 2021. preprint open access arXiv:2108.05320 cl-informatik.uibk.ac.at

Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer. "Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Drive Search Using Cylindrical Algebraic Coverings". Journal of Logical and Algebraic Methods in Programming 119 (2021) preprint open access 10.1016/j.jlamp.2020.100633

Gereon Kremer, Erika Ábrahám. "Fully Incremental Cylindrical Algebraic Decomposition". Journal of Symbolic Computation 100 (2020) preprint 10.1016/j.jsc.2019.07.018

Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer, Zak Tonks. "New Opportunities for the Formal Proof of Computational Real Geometry?". In Satisfiability Checking and Symbolic Computation (SC² 2020), CEUR Workshop Proceedings vol. 2752. 2020. open access arXiv:2004.04034 Vol-2752/paper13.pdf

Gereon Kremer. "Cylindrical Algebraic Decomposition for Nonlinear Arithmetic Problems". Dissertation. RWTH Aachen University, 2020. preprint open access 10.18154/rwth-2020-05913

Gereon Kremer, Erika Ábrahám, Vijay Ganesh. "On the Proof Complexity of MCSAT". In Satisfiability Checking and Symbolic Computation (SC² 2019) at SIAM AG, CEUR Workshop Proceedings vol. 2460. 2019. preprint open access arXiv:2109.01585 Vol-2460/paper3.pdf 10.48550/arXiv.2109.01585

Jasper Nalbach, Gereon Kremer, Erika Ábrahám. "On Variable Orderings in MCSAT for Non-linear Real Arithmetic (extended abstract)". In Satisfiability Checking and Symbolic Computation (SC² 2019) at SIAM AG, CEUR Workshop Proceedings vol. 2460. 2019. preprint open access Vol-2460/paper5.pdf

Gereon Kremer, Erika Ábrahám. "Modular strategic SMT solving with SMT-RAT". Acta Universitatis Sapientiae, Informatica 10 (1 2018) preprint open access 10.2478/ausi-2018-0001

Rebecca Haehn, Gereon Kremer, Erika Ábrahám. "Evaluation of Equational Constraints for CAD in SMT Solving". In Satisfiability Checking and Symbolic Computation (SC² 2018) at FLoC, CEUR Workshop Proceedings vol. 2189, pp. 19-32. 2018. preprint open access Vol-2189/paper10.pdf

Gereon Kremer. "Computer Algebra and Computer Science". In Applications of Computer Algebra (ACA 2018), p. 27. 2018. preprint 10.15304/9788416954872

Erika Ábrahám, Gereon Kremer. "SMT Solving for Arithmetic Theories: Theory and Tool Support". In Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2017), pp. 1-8. 2017. preprint 10.1109/SYNASC.2017.00009

Erika Ábrahám, Jasper Nalbach, Gereon Kremer. "Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework". In Satisfiability Checking and Symbolic Computation (SC² 2017) at ISSAC, CEUR Workshop Proceedings vol. 1974. 2017. preprint open access Vol-1974/EAb.pdf

Tarik Viehmann, Gereon Kremer, Erika Ábrahám. "Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving". In Satisfiability Checking and Symbolic Computation (SC² 2017) at ISSAC, CEUR Workshop Proceedings vol. 1974. 2017. preprint open access Vol-1974/RP2.pdf

Erika Ábrahám, Florian Corzilius, Einar Broch Johnsen, Gereon Kremer, Jacopo Mauro. "Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies". In Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016), LNCS vol. 9984, pp. 229-245. 2016. preprint 10.1007/978-3-319-47677-3_15

Gereon Kremer, Florian Corzilius, Erika Ábrahám. "A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic". In Computer Algebra in Scientific Computing (CASC 2016), LNCS vol. 9890, pp. 315-335. 2016. preprint 10.1007/978-3-319-45641-6_21

Erika Ábrahám, Gereon Kremer. "Satisfiability Checking: Theory and Applications". In Software Engineering and Formal Methods (SEFM 2016), LNCS vol. 9763, pp. 9-23. 2016. preprint 10.1007/978-3-319-41591-8_2

Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp, Erika Ábrahám. "SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving". In Theory and Applications of Satisfiability Testing (SAT 2015), LNCS vol. 9340, pp. 360-368. 2015. preprint 10.1007/978-3-319-24318-4_26

Gereon Kremer. "Isolating Real Roots Using Adaptable-Precision Interval Arithmetic". Master's thesis. RWTH Aachen University, 2013. preprint ths.rwth-aachen.de

Gereon Kremer. "Syntactic and Semantic Analysis of Hyperedge Replacement Grammars for Heap Abstraction". Bachelor's thesis. RWTH Aachen University, 2011. preprint moves.rwth-aachen.de