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

Publications

2019
fulltext PDF [bibtex] [issue] Jasper Nalbach, Gereon Lukas 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] [issue] Gereon Lukas 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] [issue] Rebecca Haehn, Gereon Lukas 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 (FLOC 2018), Volume 2189 of CEUR Workshop Proceedings, pages 19-32, RWTH Aachen, 2018.
DOI fulltext PDF [bibtex] [issue] Gereon Lukas Kremer, Erika Ábrahám. Modular strategic SMT solving with SMT-RAT, Acta Universitatis Sapientiae / Informatica 10 (1), pages 5-25, 2018.
2016
DOI fulltext PDF [bibtex] [issue] 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.
2017
fulltext PDF [bibtex] [issue] Tarik Viehmann, Gereon Lukas 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, CEUR-WS.org, 2017.
fulltext PDF [bibtex] [issue] Erika Ábrahám, Jasper Nalbach, Gereon Lukas 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, CEUR-WS.org, 2017.
2016
DOI [bibtex] [issue] Erika Ábrahám, Gereon Lukas Kremer. Satisfiability Checking : Theory and Applications, Software Engineering and Formal Methods, Volume 9763 of LNCS, pages 9-23, Springer, 2016.
DOI [bibtex] [issue] 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, Volume 9984 of LNCS, pages 229-245, Springer, 2016.
2015
DOI [bibtex] [issue] 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'15), Volume 9340 of LNCS, pages 360-368, Springer, 2015.

Selected Talks

2017
DownloadLinkGereon Kremer. Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving, Talk at the 2nd International Workshop on Satisfiability Checking and Symbolic Computation, 29th July 2017, Kaiserslautern, Germany, 2017.
2016
Gereon Kremer. A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic, Conference Presentation at 18th Int. Workshop on Computer Algebra in Scientific Computing (CASC'16), Bucharest, Romania, 2016.
2015
Florian Corzilius, Gereon Kremer. SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving, Talk at Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471), 2015.
2014
Gereon Kremer. Using Cylindrical Algebraic Decomposition in Satisfiability Modulo Theories, Talk at 8th Joint Workshop of the German Research Training Groups in Computer Science, 2014.
Gereon Kremer, Sebastian Junges. Satisfiability Modulo Real Arithmetic - SMT-Solving with CAD and Gröbner Bases, Talk at Joint Workshop of Research Training Groups PUMA and AlgoSyn, 2014.