Gereon Kremer

Research Scientist in Computer Science
Stanford University

I'm a postdoctoral researcher at Stanford University in Clark Barrett's group. Previously, I was a researcher at RWTH Aachen University in the Theory of Hybrid Systems groups led by Erika Ábrahám where I also did my PhD about using Cylindrical Algebraic Decomposition for SMT solving.

My research interests include

  • Satisfiability Modulo Theories (SMT)
  • Techniques for Nonlinear Arithmetic
  • Cylindrical Algebraic Decomposition
  • Automated Testing and Debugging

Education

  • Doctor of natural sciences (Dr. rer. nat) in Computer Science, 2020

    RWTH Aachen University

  • MSc in Computer Science, 2013

    RWTH Aachen University

  • BSc in Computer Science, 2011

    RWTH Aachen University

Publications

see all publications
  • 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) download open access 10.1016/j.jlamp.2020.100633
  • 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. download 10.1145/3452143.3465538
  • Gereon Kremer, Aina Niemetz and 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. download open access 10.1007/978-3-030-81688-9_11
  • 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. download open access cl-informatik.uibk.ac.at
  • Gereon Kremer, Erika Ábrahám. "Fully Incremental Cylindrical Algebraic Decomposition". Journal of Symbolic Computation 100 (2020) download 10.1016/j.jsc.2019.07.018
  • Gereon Kremer. "Cylindrical Algebraic Decomposition for Nonlinear Arithmetic Problems". Dissertation. RWTH Aachen University, 2020. download open access 10.18154/rwth-2020-05913
  • 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, 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. download open access Vol-2460/paper3.pdf
  • 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. download open access Vol-2460/paper5.pdf

Projects

active
cvc5

An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems

cvc5/cvc5
cvc5.github.io
active
ddSMT

A delta debugger for SMT-LIBv2

ddsmt/ddSMT
ddsmt.readthedocs.io
supported
SMT-RAT

An SMT solver with special focus on Nonlinear Real Arithmetic

smtrat/smtrat
supported
CArL

A C++ library for Computer ARithmetic and Logic

smtrat/carl
active
libpoly

A C library for manipulating polynomials

SRI-CSL/libpoly
deprecated
CVC4

An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems

CVC4/CVC4-archived
cvc4.github.io
download
Techniques for NRA in SMT

May 2021, Automated Reasoning in the Class, Training on SMT Solving

download
Techniques for NRA

October 2020, Software Research Lunch, Stanford University, USA

download
Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings

July 2020, International Congress on Mathematical Software, TU Braunschweig, Germany

Cylindrical Algebraic Decomposition for Nonlinear Arithmetic Problems

March 2020, RWTH Aachen University, Germany

download
On the proof complexity of MCSAT

July 2019, Satisfiability Checking and Symbolic Computation, Universität Bern, Switzerland

download
Incremental CAD

July 2018, International Congress on Mathematical Software, University of Notre Dame, USA

download
Computer Algebra and Computer Science

June 2018, Applications of Computer Algebra, University of Santiago de Compostela, Spain

Other activities

Teaching assistance
Conference reviews

CAV'21, ISSAC'21, FMCAD'20, WRLA'20, FMCAD'19, iFM'19, LPAR-22, NFM'18, HSCC'17, MACIS'17, TMPA'17, VMCAI'17, FM'16, SMT'16, ATVA'15, FM'15, TACAS'15, VMCAI'15, FTSCS'14, HSCC'14

Journal reviews

JSC 2016, 2018, 2019, FMSD 2021

PC member

SMT Workshop 2021