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
[bibtex] [issue] Erika Ábrahám, Gereon Kremer, James Davenport, Matthew England. 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, Elsevier Science, 2020.
DOI fulltext PDF [bibtex] [issue] Gereon Kremer. Cylindrical algebraic decomposition for nonlinear arithmetic problems, PhD Thesis, RWTH Aachen University, Volume 2020-04 of Aachener Informatik-Berichte, 1 Online-Ressource (204 Seiten) : Illustrationen, Diagramme, 2020.
2019
fulltext PDF [bibtex] [issue] Erika Ábrahám, Gereon Kremer, 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 Seiten, RWTH Aachen, 2019.
DOI fulltext PDF [bibtex] [issue] Erika Ábrahám, Gereon Kremer, Jasper Nalbach. On Variable Orderings in MCSAT for Non-linear Real Arithmetic, 4th Workshop on Satisfiability Checking and Symbolic Computation (SC-square), Volume 2460 of CEUR Workshop Proceedings, 7 Seiten, RWTH Aachen, 2019.
DOI [bibtex] [issue] Erika Ábrahám, Gereon Kremer. Fully Incremental Cylindrical Algebraic Decomposition, Journal of symbolic computation 100, pages 11-37, Elsevier, 2019.
2018
DOI fulltext PDF [bibtex] [issue] Erika Ábrahám, Gereon Kremer. Modular strategic SMT solving with SMT-RAT, Acta Universitatis Sapientiae / Informatica 10 (1), pages 5-25, De Gruyter Open, 2018.
fulltext PDF [bibtex] [issue] Erika Ábrahám, Gereon Kremer, Rebecca Haehn. 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, [19]-32, RWTH Aachen, 2018.
2017
[bibtex] [issue] Erika Ábrahám, Gereon Kremer, Jasper Nalbach. 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 Seiten, RWTH Aachen, 2017.
fulltext PDF [bibtex] [issue] Erika Ábrahám, Gereon Kremer, Tarik Viehmann. 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 Seiten, RWTH Aachen, 2017.
DOI [bibtex] [issue] Erika Ábrahám, Gereon Lukas Kremer. SMT Solving for Arithmetic Theories, 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2017), 1-8, IEEE, 2017.
2016
DOI fulltext PDF [bibtex] [issue] Erika Ábrahám, Florian Corzilius, Gereon Kremer. 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, 315-335, Springer, 2016.
DOI [bibtex] [issue] Einar Broch Johnsen, Erika Ábrahám, Florian Corzilius, Gereon Kremer, Jacopo Mauro. Zephyrus2, International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016), Volume 9984 of LNCS, 229-245, Springer, 2016.
DOI [bibtex] [issue] Erika Ábrahám, Gereon Kremer. Satisfiability Checking, Software Engineering and Formal Methods : 14th International Conference (SEFM 2016), Volume 9763 of LNCS, 9-23, Springer, 2016.
2015
DOI [bibtex] [issue] Erika Ábrahám, Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp. SMT-RAT, International Conference on Theory and Applications of Satisfiability Testing (SAT 2015), Volume 9340 of LNCS, 360-368, Springer, 2015.