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

2018
Link
[bibtex]
Rebecca Haehn, Gereon Kremer, Erika Abraham. Evaluation of Equational Constraints for CAD in SMT Solving. Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation, Volume 2189 of CEUR Workshop Proceedings, pages 19–32, CEUR-WS.org, 2018.
Link
[bibtex]
Gereon Kremer, Erika Abraham. Modular strategic SMT solving with SMT-RAT. Acta Universitatis Sapientiae, Informatica 10(1), pages 5–25, 2018.
2017
Download
[bibtex]
Erika Abraham, Gereon Kremer. SMT Solving for Arithmetic Theories: Theory and Tool Support. Proceedings of the 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2017), pages 1–8, IEEE, 2017.
Download
[bibtex]
Tarik Viehmann, Gereon Kremer, Erika Abraham. Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving. Proc. of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation, Volume 1974 of CEUR Workshop Proceedings, CEUR-WS.org, 2017.
Link
[bibtex]
Erika Abraham, Jasper Nalbach, Gereon Kremer. Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework. Proc. of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation, Volume 1974 of CEUR Workshop Proceedings, CEUR-WS.org, 2017.
2016
Download
[bibtex]
Gereon Kremer, Florian Corzilius, Erika Abraham. A Generalised Branch-and-Bound Approach and its Application in SAT Modulo Nonlinear Integer Arithmetic. 18th International Workshop on Computer Algebra in Scientific Computing (CASC'16), Volume 9890 of LNCS, pages 315-335, Springer, 2016.
DOI
[bibtex]
Erika Abraham, Gereon Kremer. Satisfiability Checking: Theory and Applications. Proceedings of the 14th International Conference on Software Engineering and Formal Methods (SEFM'16), Volume 9763 of LNCS, pages 9–23, Springer International Publishing, 2016.
Download
[bibtex]
Erika Abraham, Florian Corzilius, Einar Broch Johnsen, Gereon Kremer, Jacopo Mauro. Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies. Dependable Software Engineering: Theories, Tools, and Applications (SETTA'16), Volume 9984 of LNCS, pages 229–245, Springer, 2016.
2015
DOI
[bibtex]
Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp, Erika Abraham. SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving. Proc. of the 18th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT'15), Volume 9340 of LNCS, pages 360–368, Springer, 2015.

Selected Talks

2017
DownloadGereon 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.