Gereon Kremer
Research Interests
- SMT solving
- Nonlinear real arithmetic
- Cylindrical Algebraic Decomposition
- Integer arithmetic
Teaching
- SS 2016: Seminar Satisfiability Checking
- SS 2016: Practical Course SMT-Solving
- WS 2015/16: Lecture Satisfiability Checking
- WS 2015/16: Practical Course SMT-Solving
- WS 2015/16: Proseminar Algorithms and Tools for Verification
- SS 2015: Practical Course SMT-Solving
- SS 2015: Seminar Satisfiability Checking
- WS 2014/15: Lecture Satisfiability Checking
- WS 2014/15: Practical Course SMT-Solving
- WS 2014/15: Proseminar Algorithms and Tools for Verification
- SS 2014: Seminar Satisfiability Checking
- SS 2014: Proseminar Wurzeln der Informatik
- WS 2013/14: Proseminar Algorithms and Tools for Verification
Publications
| 2026 | |
|---|---|
| DOI Details | Jasper Nalbach and Gereon Kremer. 2026. Extensions of the Cylindrical Algebraic Covering Method for Quantifiers. Mathematics in computer science 20, 1 (2026), 7. |
| 2024 | |
| DOI Details | Jasper Nalbach and Gereon Kremer. 2024. Extensions of the Cylindrical Algebraic Covering Method for Quantifiers. arXiv:2411.03070. |
| 2023 | |
| Details | Gereon Kremer and Jasper Nalbach. 2023. Cylindrical Algebraic Coverings for Quantifiers. In Proceedings of the 7th SC-Square Workshop, CEUR-WS Proceedings (CEUR workshop proceedings, Vol. 3458). RWTH-Aachen, Aachen, Germany, 9 pages. |
| 2021 | |
| DOI Details | Erika Ábrahám, James H. Davenport, Matthew England, and Gereon Kremer. 2021. Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings. Journal of Logical and Algebraic Methods in Programming 119 (2021), 100633. |
| DOI Details | Jasper Nalbach, Erika Ábrahám, and Gereon Kremer. 2021. Extending the Fundamental Theorem of Linear Programming for Strict Inequalities. In ISSAC '21 : Proceedings of the 2021 International Symposium on Symbolic and Algebraic Computation : July 18-23, 2021, Virtual Event, Russian Federation (ACM Conferences). Association for Computing Machinery, New York, NY, United States, 313–320. |
| DOI Details | Erika Ábrahám, James H. Davenport, Matthew England, and Gereon Kremer. 2021. Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic. arXiv:2108.05320. |
| DOI Details | Gereon Kremer, Erika Ábrahám, and Vijay Ganesh. 2021. On the proof complexity of MCSAT. arXiv:2109.01585. |
| DOI Details | Gereon Kremer, Erika Ábrahám, Matthew England, and James H. Davenport. 2021. On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving. In 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing : SYNASC 2021 : virtual conference, 7-10 December 2021. IEEE, Piscataway, NJ, 37–39. |
| 2020 | |
| DOI Details | Gereon Kremer and Erika Ábrahám. 2020. Fully Incremental Cylindrical Algebraic Decomposition. Journal of symbolic computation 100 (2020), 11–37. |
| DOI Details | Erika Ábrahám, James H. Davenport, Matthew England, and Gereon Kremer. 2020. Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings. arXiv:2003.05633. |
| DOI Details | Gereon Kremer. 2020. Cylindrical algebraic decomposition for nonlinear arithmetic problems. Ph.D. Dissertation. RWTH Aachen University, Aachen. |
| DOI Details | Jasper Nalbach. 2020. A novel adaption of the Simplex algorithm for linear real arithmetic. Master's thesis. RWTH Aachen University, Aachen. |
| DOI Details | Erika Ábrahám, James Davenport, Matthew England, Gereon Kremer, and Zak Tonks. 2020. New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract). In PAAR+SC-Square 2020: Practical Aspects of Automated Reasoning and Satisfiability Checking and Symbolic Computation Workshop 2020 : joint proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020 : co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020) : Paris, France, June-July, 2020 (virtual) (CEUR workshop proceedings, Vol. 2752). RWTH Aachen, Aachen, Germany, 178–188. |
| DOI Details | Erika Ábrahám, James Davenport, Matthew England, Gereon Kremer, and Zak Tonks. 2020. New Opportunities for the Formal Proof of Computational Real Geometry? arXiv:2004.04034. |
| 2019 | |
| Details | Gereon Kremer, Erika Ábrahám, and Vijay Ganesh. 2019. On the Proof Complexity of MCSAT. In SC-square 2019 : Satisfiability Checking and Symbolic Computation 2019 : Proceedings of the 4th SC-Square Workshop co-located with the SIAM Conference on Applied Algebraic Geometry (SIAM AG 2019) : Bern, Switzerland, 10th July 2019 (CEUR workshop proceedings, Vol. 2460). RWTH-Aachen, Aachen, Germany, 10 pages. |
| DOI Details | Jasper Nalbach, Gereon Kremer, and Erika Ábrahám. 2019. On Variable Orderings in MCSAT for Non-linear Real Arithmetic : (extended abstract). In SC-square 2019 : Satisfiability Checking and Symbolic Computation 2019 : Proceedings of the 4th SC-Square Workshop co-located with the SIAM Conference on Applied Algebraic Geometry (SIAM AG 2019) : Bern, Switzerland, 10th July 2019 (CEUR workshop proceedings, Vol. 2460). RWTH-Aachen, Aachen, Germany, 7 pages. |
| 2018 | |
| DOI Details | Gereon Kremer and Erika Ábrahám. 2018. Modular strategic SMT solving with SMT-RAT. Acta Universitatis Sapientiae / Informatica 10, 1 (2018), 5–25. |
| Details | Rebecca Haehn, Gereon Kremer, and Erika Ábrahám. 2018. Evaluation of Equational Constraints for CAD in SMT Solving. In Satisfiability checking and symbolic computation : SC-Square 2018 : proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation, co-located with Federated Logic Conference (FLOC 2018) : Oxford, UK, July 11, 2018 (CEUR workshop proceedings, Vol. 2189). RWTH-Aachen, Aachen, Germany, 19–32. |
| 2017 | |
| Details | Erika Ábrahám, Jasper Nalbach, and Gereon Kremer. 2017. Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework. In Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation co-located with the 42nd International Symposium on Symbolic and Algebraic Computation (ISSAC 2017), Kaiserslautern, Germany, July 29, 2017 (CEUR workshop proceedings, Vol. 1974). RWTH Aachen, Aachen, Germany, 12 pages. |
| Details | Tarik Viehmann, Gereon Kremer, and Erika Ábrahám. 2017. Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving. In [2nd International Workshop on Satisfiability Checking and Symbolic Computation, SC2, 2017-07-29 - 2017-07-29, Kaiserslautern, Germany (CEUR workshop proceedings, Vol. 1974). RWTH Aachen, Aachen, Germany, 15 pages. |
| DOI Details | Erika Ábrahám and Gereon Kremer. 2017. SMT Solving for Arithmetic Theories: Theory and Tool Support. In 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. IEEE, 1–8. |
| 2016 | |
| DOI Details | Gereon Kremer, Florian Corzilius, and Erika Ábrahám. 2016. A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic. In Computer algebra in scientific computing : 18th international workshop, CASC 2016, Bucharest, Romania, September 19-23, 2016 : proceedings (Lecture Notes in Computer Science, Vol. 9890). Springer International Publishing, Cham, 315–335. |
| DOI Details | Erika Ábrahám, Florian Corzilius, Einar Broch Johnsen, Gereon Kremer, and Jacopo Mauro. 2016. Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies. In Dependable software engineering : theories, tools, and applications : second international symposium, SETTA 2016, Beijing, China, November 9-11, 2016 : proceedings (Lecture Notes in Computer Science, Vol. 9984). Springer International Publishing, Cham, 229–245. |
| DOI Details | Erika Ábrahám and Gereon Kremer. 2016. Satisfiability Checking : Theory and Applications. In Software engineering and formal methods : 14th international conference, SEFM 2016, held as part of STAF 2016, Vienna, Austria, July 4-8, 2016 : proceedings (Lecture Notes in Computer Science, Vol. 9763). Springer International Publishing ; Imprint: Springer, Cham ; s.l., 9–23. |
| 2015 | |
| DOI Details | Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp, and Erika Ábrahám. 2015. SMT-RAT : an Open Source C++ Toolbox for Strategic and Parallel SMT Solving. In Theory and Applications of Satisfiability Testing : SAT 2015 ; 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings (Lecture Notes in Computer Science, Vol. 9340). Springer International Publishing, Cham, 360–368. |
| Show all | |