Gereon Kremer

kremer
Email
gereon.kremer at cs.rwth-aachen.de
Phone
+49 241 80 21243
Address
Room 4228
Ahornstraße 55
D-52074 Aachen

Research Interests

  • SMT solving
  • Nonlinear real arithmetic
  • Cylindrical Algebraic Decomposition
  • Integer arithmetic

Teaching

2020
DOI [bibtex] A. M. Golubev, J. Nuss, Gereon Kremer, E. E. Gordon, M.-H. Whangbo, C. Ritter, Lina Apitius, Stefan Weßel. Two-dimensional magnetism in α − CuV 2 O 6, Physical review / B 102 (1), pages 014436, 2020.
DOI fulltext PDF [bibtex] Gereon Kremer. Cylindrical algebraic decomposition for nonlinear arithmetic problems, PhD Thesis, RWTH Aachen University, Volume 2020-04 of Aachener Informatik-Berichte, 204 pages, 2020.
restricted URL PDF [bibtex] Erika Ábrahám, James Davenport, Matthew England, Gereon Kremer. 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 , 2020.
2019
DOI restricted URL PDF [bibtex] Gereon Kremer, Erika Ábrahám. Fully Incremental Cylindrical Algebraic Decomposition, Journal of symbolic computation 100, pages 11-37, 2019.
DOI fulltext PDF [bibtex] Jasper Nalbach, Gereon Kremer, Erika Ábrahám. On Variable Orderings in MCSAT for Non-linear Real Arithmetic : (extended abstract), 4th Workshop on Satisfiability Checking and Symbolic Computation (SC-square), Volume 2460 of CEUR Workshop Proceedings, 7 pages, RWTH Aachen, 2019.
fulltext PDF [bibtex] Gereon Kremer, Erika Ábrahám, Vijay Ganesh. On the Proof Complexity of MCSAT, 4th Workshop on Satisfiability Checking and Symbolic Computation (SC-square), Volume 2460 of CEUR Workshop Proceedings, 10 pages, RWTH Aachen, 2019.
2018
fulltext PDF [bibtex] Rebecca Haehn, Gereon Kremer, Erika Ábrahám. Evaluation of Equational Constraints for CAD in SMT Solving, 3rd Workshop on Satisfiability Checking and Symbolic Computation co-located with Federated Logic Conference (SC-Square 2018), Volume 2189 of CEUR Workshop Proceedings, pages 19-32, RWTH Aachen, 2018.
DOI fulltext PDF [bibtex] Gereon Kremer, Erika Ábrahám. Modular strategic SMT solving with SMT-RAT, Acta Universitatis Sapientiae / Informatica 10 (1), pages 5-25, 2018.
2017
DOI restricted URL PDF [bibtex] Erika Ábrahám, Gereon Lukas Kremer. SMT Solving for Arithmetic Theories: Theory and Tool Support, 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2017), pages 1-8, IEEE, 2017.
fulltext PDF [bibtex] Tarik Viehmann, Gereon Kremer, Erika Ábrahám. Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving, 2nd International Workshop on Satisfiability Checking and Symbolic Computation (SC2), Volume 1974 of CEUR Workshop Proceedings, 15 pages, RWTH Aachen, 2017.
restricted URL PDF [bibtex] Erika Ábrahám, Jasper Nalbach, Gereon Kremer. Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework, 2nd International Workshop on Satisfiability Checking and Symbolic Computation (SC2), Volume 1974 of CEUR Workshop Proceedings, 12 pages, RWTH Aachen, 2017.
2016
DOI fulltext PDF [bibtex] Gereon Kremer, Florian Corzilius, Erika Ábrahám. A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic, International Workshop on Computer Algebra in Scientific Computing (CASC16), Volume 9890 of LNCS, pages 315-335, Springer, 2016.
DOI [bibtex] Erika Ábrahám, Gereon Kremer. Satisfiability Checking : Theory and Applications, Software Engineering and Formal Methods : 14th International Conference (SEFM 2016), Volume 9763 of LNCS, pages 9-23, Springer, 2016.
DOI [bibtex] Erika Ábrahám, Florian Corzilius, Einar Broch Johnsen, Gereon Kremer, Jacopo Mauro. Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies, International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016), Volume 9984 of LNCS, pages 229-245, Springer, 2016.
2015
DOI [bibtex] Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp, Erika Ábrahám. SMT-RAT : an Open Source C++ Toolbox for Strategic and Parallel SMT Solving, International Conference on Theory and Applications of Satisfiability Testing (SAT 2015), Volume 9340 of LNCS, pages 360-368, Springer, 2015.