I'm working as a researcher in the SMT team at Certora. Certora offers one of the leading solutions for formally verifying Ethereum smart contracts used for decentralized financial applications. The focus of the SMT team is to improve the SMT backend of the Certora Verification Tool to enhance scalability, robustness and usefulness for the end user.
Previously, I was a postdoctoral researcher at the Center for Automated Reasoning at Stanford University advised by Clark Barrett after working as a researcher at RWTH Aachen University in the Theory of Hybrid Systems group led by Erika Ábrahám where I also did my PhD about using Cylindrical Algebraic Decomposition for SMT solving.
research interests
- Satisfiability Modulo Theories (SMT)
- Techniques for Nonlinear Arithmetic
- Cylindrical Algebraic Decomposition
- Automated Testing and Debugging
Education
-
PhD (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
Projects
Certora Prover
Verifies EVM bytecode with respect to a specification written in the Certora Verification Language
docs.certora.com
cvc5
An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems
cvc5/cvc5cvc5.github.io
CVC4
An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems
CVC4/CVC4-archivedcvc4.github.io
Talks
see all talksSatisfiability Modulo Finite Fields // The Certora Prover
September 2024, TUM Blockchain Conference, Munich, Germany
Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver
August 2022, International Joint Conference on Automated Reasoning, Haifa, Israel
Cylindrical Algebraic Coverings for Quantifiers
August 2022, Satisfiability Checking and Symbolic Computation, Haifa, Israel
Satisfiability Modulo Theories for Arithmetic Problems
June 2022, Global Virtual SageDays, the world
Formal proofs for Cylindrical Algebraic Coverings
February 2022, New Perspectives in Symbolic Computation and Satisfiability Checking, Dagstuhl, Germany
On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving
December 2021, Symbolic and Numeric Algorithms for Scientific Computing, West University of Timisoara, Romania
Implementing arithmetic over algebraic numbers: A tutorial for Lazard's lifting scheme
December 2021, Symbolic and Numeric Algorithms for Scientific Computing, West University of Timisoara, Romania
Publications
see all 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
Other activities
Conference reviews
FM'24, SCSC'24, SCSC'23, NFM'23, SCSC'22, IJCAR'22, CAV'21, ISSAC'21, SMT'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, 2024, MCS 2024
Teaching assistance
- Satisfiability Checking Lecture 2014/15 2015/16 2016/17 2017/18 2019/20
- SMT-Solving Practical course UF 2014/15 UF 2015 UF 2015/16 UF 2016 ICP 2017 Simplex 2017 ICP 2018 UF 2018/19 UF 2019
- Hybrid Systems Verification Seminar 2014/15 2016/17
- Satisfiability Checking Seminar 2014 2015 2015/16 2016 2016/17 2017 2018 2019
- Algorithms and Tools for Verification Proseminar 2013/14 2014 2014/15 2015/16
Supervised thesis projects
- Master download A novel adaption of the simplex algorithm for linear real arithmetic. Jasper Nalbach, 2020, supervised with Erika Ábrahám.
- Master download Conflict driven cylindrical algebraic coverings for nonlinear arithmetic in SMT solving. Hanna Franzen, 2020, supervised with Erika Ábrahám.
- Bachelor download SMT-basierte Lösung reell-algebraischer Probleme mittels Linearisierung. Denis Kuksaus, 2019, supervised with Erika Ábrahám.
- Master download Incremental linearization for SAT modulo real arithmetic solving. Aklima Zaman, 2019, supervised with Erika Ábrahám.
- Master download Linearization techniques for nonlinear arithmetic problems in SMT. Ömer Sali, 2018, supervised with Erika Ábrahám.
- Bachelor download Quantifier elimination by cylindrical algebraic decomposition. Tom Neuhäuser, 2018, supervised with Erika Ábrahám.
- Master download Using equational constraints in an incremental CAD projection. Rebecca Haehn, 2018, supervised with Erika Ábrahám.
- Master download Using single CAD cells as explanations in MCSAT-style SMT solving. Malte Neuß, 2018, supervised with Erika Ábrahám.
- Bachelor download Using Fourier-Motzkin variable elimination for MCSAT explanations in SMT-RAT. Lorena Calo Bartolomé, 2018, supervised with Erika Ábrahám.
- Master download Automated optimization in production planning. Henri Lotze, 2018, supervised with Erika Ábrahám.
- Bachelor download Implementing an incremental solver for difference logic. Christopher Lösbrock, 2018, supervised with Erika Ábrahám, Matthias Volk.
- Bachelor download Computing minimal infeasible subsets for the cylindrical algebraic decomposition. Wanja Hentze, 2017, supervised with Erika Ábrahám.
- Bachelor download Solving pseudo-Boolean constraints. Marta Grobelna, 2017, supervised with Erika Ábrahám.
- Bachelor download Using Thom encodings for real algebraic numbers in the cylindrical algebraic decomposition. Tobias Winkler, 2016, supervised with Erika Ábrahám.
- Bachelor download Comparing different projection operators in the cylindrical algebraic decomposition for SMT solving. Tarik Viehmann, 2016, supervised with Erika Ábrahám.
- Bachelor download SMT-based planning for autonomous robot fleets. Leonard Korp, 2016, supervised with Erika Ábrahám, Francesco Leofante.
- Bachelor download Generation of infeasible subsets in less-lazy SMT-solving for the theory of uninterpreted functions. Lukas Neuberger, 2015, supervised with Erika Ábrahám.
- Master download Bitvectors in SMT-RAT and their application to integer arithmetics. Andreas Krüger, 2015, supervised with Erika Ábrahám.