Gereon Kremer | Theory of Hybrid Systems

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

2024
[bibtex] @unpublished{ECACMQ2024, title = {Extensions of the Cylindrical Algebraic Covering Method for Quantifier}, author = {Jasper Kurt Ferdinand Nalbach and Gereon Kremer}, type = {Preprint}, year = {2024}, doi = {10.48550/ARXIV.2411.03070}, url = { https://arxiv.org/abs/2411.03070}, }× [issue]	Jasper Kurt Ferdinand Nalbach, Gereon Kremer. Extensions of the Cylindrical Algebraic Covering Method for Quantifier, 2024. https://arxiv.org/abs/2411.03070
2023
[bibtex] @conference{CACQ2023, title = {Cylindrical Algebraic Coverings for Quantifiers}, author = {Gereon Kremer and Jasper Kurt Ferdinand Nalbach}, booktitle = {CEUR Workshop Proceedings}, volume = {3458}, pages = {9 Seiten}, type = {Conference Paper}, year = {2023}, url = { https://publications.rwth-aachen.de/record/956001}, }× [issue]	Gereon Kremer, Jasper Kurt Ferdinand Nalbach. Cylindrical Algebraic Coverings for Quantifiers, 7. International Workshop on Satisfiability Checking and Symbolic Computation (SC² 2022), Volume 3458 of CEUR Workshop Proceedings, 9 Seiten, 2023.
2021
[bibtex] @article{D2021, title = {Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings}, author = {Erika Ábrahám and James H. Davenport and Matthew England and Gereon Kremer}, publisher = {Elsevier Science}, journal = {Journal of Logical and Algebraic Methods in Programming}, volume = {119}, pages = {pages 100633}, type = {Journal Article}, year = {2021}, doi = {10.1016/j.jlamp.2020.100633}, url = { https://publications.rwth-aachen.de/record/816049}, }× [issue]	Erika Ábrahám, James H. 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 119, pages 100633, Elsevier Science, 2021.
[bibtex] @conference{EFTLPSI2021, title = {Extending the Fundamental Theorem of Linear Programming for Strict Inequalities}, author = {Jasper Kurt Ferdinand Nalbach and Erika Ábrahám and Gereon Kremer}, publisher = {Association for Computing Machinery}, booktitle = {ACM Conferences}, pages = {313-320}, type = {Conference Paper}, year = {2021}, doi = {10.1145/3452143.3465538}, url = { https://publications.rwth-aachen.de/record/823081}, }× [issue]	Jasper Kurt Ferdinand Nalbach, Erika Ábrahám, Gereon Kremer. Extending the Fundamental Theorem of Linear Programming for Strict Inequalities, International Symposium on Symbolic and Algebraic Computation (ISSAC '21), ACM Conferences, 313-320, Association for Computing Machinery, 2021.
[bibtex] @unpublished{PUSTCQFNLRA2021, title = {Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic}, author = {Erika Ábrahám and James H. Davenport and Matthew England and Gereon Kremer}, pages = {5 Seiten}, type = {Preprint}, year = {2021}, doi = {10.48550/ARXIV.2108.05320}, url = { https://arxiv.org/abs/2108.05320}, }× [issue]	Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer. Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic, 5 Seiten, 2021. https://arxiv.org/abs/2108.05320
[bibtex] @unpublished{OM2021, title = {On the proof complexity of MCSAT}, author = {Gereon Kremer and Erika Ábrahám and Vijay Ganesh}, type = {Preprint}, year = {2021}, doi = {10.48550/ARXIV.2109.01585}, url = { https://arxiv.org/abs/2109.01585}, }× [issue]	Gereon Kremer, Erika Ábrahám, Vijay Ganesh. On the proof complexity of MCSAT, 2021. https://arxiv.org/abs/2109.01585
[bibtex] @conference{OICACSMTS2021, title = {On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving}, author = {Gereon Kremer and Erika Ábrahám and Matthew England and James H. Davenport}, publisher = {IEEE}, pages = {37-39}, type = {Conference Paper}, year = {2021}, doi = {10.1109/SYNASC54541.2021.00018}, url = { https://publications.rwth-aachen.de/record/846648}, }× [issue]	Gereon Kremer, Erika Ábrahám, Matthew England, James H. Davenport. On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving, 23. International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 37-39, IEEE, 2021.
2020
[bibtex] @unpublished{DCNLRACCDSUCAC2020, title = {Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings}, author = {Erika Ábrahám and James H. Davenport and Matthew England and Gereon Kremer}, publisher = {Elsevier Science}, pages = {41 Seiten}, type = {Preprint}, year = {2020}, doi = {10.48550/ARXIV.2003.05633}, url = { https://arxiv.org/abs/2003.05633}, }× [issue]	Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer. Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings, 41 Seiten, Elsevier Science, 2020. https://arxiv.org/abs/2003.05633
[bibtex] @phdthesis{C2020, title = {Cylindrical algebraic decomposition for nonlinear arithmetic problems}, author = {Gereon Kremer}, booktitle = {Aachener Informatik-Berichte}, volume = {2020-04}, institution = {RWTH Aachen University}, pages = {1 Online-Ressource (204 Seiten) : Illustrationen, Diagramme}, type = {PhD Thesis}, year = {2020}, doi = {10.18154/RWTH-2020-05913}, url = { https://publications.rwth-aachen.de/record/792185}, }× [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.
[bibtex] @misc{NOFPCRGEA2020, title = {New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract)}, author = {Erika Ábrahám and James Davenport and Matthew England and Gereon Kremer and Zak Tonks}, publisher = {RWTH Aachen}, booktitle = {CEUR Workshop Proceedings}, volume = {2752}, pages = {178-188}, type = {Invited Abstract}, year = {2020}, doi = {10.18154/RWTH-2021-09565}, url = { https://publications.rwth-aachen.de/record/833961}, }× [issue]	Erika Ábrahám, James Davenport, Matthew England, Gereon Kremer, Zak Tonks. New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract), Volume 2752 of CEUR Workshop Proceedings, 178-188, RWTH Aachen, 2020.
[bibtex] @unpublished{NOFPCRG2020, title = {New Opportunities for the Formal Proof of Computational Real Geometry?}, author = {Erika Ábrahám and James Davenport and Matthew England and Gereon Kremer and Zak Tonks}, pages = {14 Seiten}, type = {Preprint}, year = {2020}, doi = {10.48550/ARXIV.2004.04034}, url = { https://arxiv.org/abs/2004.04034}, }× [issue]	Erika Ábrahám, James Davenport, Matthew England, Gereon Kremer, Zak Tonks. New Opportunities for the Formal Proof of Computational Real Geometry?, 14 Seiten, 2020. https://arxiv.org/abs/2004.04034
2019
[bibtex] @conference{OPCM2019, title = {On the Proof Complexity of MCSAT}, author = {Gereon Kremer and Erika Ábrahám and Vijay Ganesh}, publisher = {RWTH Aachen}, booktitle = {CEUR Workshop Proceedings}, volume = {2460}, pages = {10 Seiten}, type = {Conference Paper}, year = {2019}, url = { https://publications.rwth-aachen.de/record/771621}, }× [issue]	Gereon Kremer, Erika Ábrahám, Vijay Ganesh. On the Proof Complexity of MCSAT, 4. Workshop on Satisfiability Checking and Symbolic Computation (SC-square), Volume 2460 of CEUR Workshop Proceedings, 10 Seiten, RWTH Aachen, 2019.
[bibtex] @conference{OVOMNRA2019, title = {On Variable Orderings in MCSAT for Non-linear Real Arithmetic: (extended abstract)}, author = {Jasper Kurt Ferdinand Nalbach and Gereon Kremer and Erika Ábrahám}, publisher = {RWTH Aachen}, booktitle = {CEUR Workshop Proceedings}, volume = {2460}, pages = {7 Seiten}, type = {Conference Paper}, year = {2019}, doi = {10.18154/RWTH-CONV-240068}, url = { https://publications.rwth-aachen.de/record/771622}, }× [issue]	Jasper Kurt Ferdinand Nalbach, Gereon Kremer, Erika Ábrahám. On Variable Orderings in MCSAT for Non-linear Real Arithmetic: (extended abstract), 4. Workshop on Satisfiability Checking and Symbolic Computation (SC-square), Volume 2460 of CEUR Workshop Proceedings, 7 Seiten, RWTH Aachen, 2019.
[bibtex] @article{FICAD2019, title = {Fully Incremental Cylindrical Algebraic Decomposition}, author = {Gereon Kremer and Erika Ábrahám}, publisher = {Elsevier}, journal = {Journal of symbolic computation}, volume = {100}, pages = {pages 11-37}, type = {Journal Article}, year = {2019}, doi = {10.1016/j.jsc.2019.07.018}, url = { https://publications.rwth-aachen.de/record/780485}, }× [issue]	Gereon Kremer, Erika Ábrahám. Fully Incremental Cylindrical Algebraic Decomposition, Journal of symbolic computation 100, pages 11-37, Elsevier, 2019.
2018
[bibtex] @article{MSSR2018, title = {Modular strategic SMT solving with SMT-RAT}, author = {Gereon Kremer and Erika Ábrahám}, publisher = {De Gruyter Open}, journal = {Acta Universitatis Sapientiae / Informatica}, volume = {10(1)}, pages = {pages 5-25}, type = {Journal Article}, year = {2018}, doi = {10.2478/ausi-2018-0001}, url = { https://publications.rwth-aachen.de/record/735737}, }× [issue]	Gereon Kremer, Erika Ábrahám. Modular strategic SMT solving with SMT-RAT, Acta Universitatis Sapientiae / Informatica 10 (1), pages 5-25, De Gruyter Open, 2018.
[bibtex] @conference{EECCSS2018, title = {Evaluation of Equational Constraints for CAD in SMT Solving}, author = {Rebecca Haehn and Gereon Kremer and Erika Ábrahám}, publisher = {RWTH Aachen}, booktitle = {CEUR Workshop Proceedings}, volume = {2189}, pages = {[19]-32}, type = {Conference Paper}, year = {2018}, url = { https://publications.rwth-aachen.de/record/753088}, }× [issue]	Rebecca Haehn, Gereon Kremer, Erika Ábrahám. Evaluation of Equational Constraints for CAD in SMT Solving, 3. 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] @conference{EVSMMCSCF2017, title = {Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework}, author = {Erika Ábrahám and Jasper Kurt Ferdinand Nalbach and Gereon Kremer}, publisher = {RWTH Aachen}, booktitle = {CEUR Workshop Proceedings}, volume = {1974}, pages = {12 Seiten}, type = {Conference Paper}, year = {2017}, url = { https://publications.rwth-aachen.de/record/713477}, }× [issue]	Erika Ábrahám, Jasper Kurt Ferdinand Nalbach, Gereon Kremer. Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework, 2. International Workshop on Satisfiability Checking and Symbolic Computation (SC2), Volume 1974 of CEUR Workshop Proceedings, 12 Seiten, RWTH Aachen, 2017.
[bibtex] @conference{CDPOCADSS2017, title = {Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving}, author = {Tarik Viehmann and Gereon Kremer and Erika Ábrahám}, publisher = {RWTH Aachen}, booktitle = {CEUR Workshop Proceedings}, volume = {1974}, pages = {15 Seiten}, type = {Conference Paper}, year = {2017}, url = { https://publications.rwth-aachen.de/record/713479}, }× [issue]	Tarik Viehmann, Gereon Kremer, Erika Ábrahám. Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving, 2. International Workshop on Satisfiability Checking and Symbolic Computation (SC2), Volume 1974 of CEUR Workshop Proceedings, 15 Seiten, RWTH Aachen, 2017.
[bibtex] @conference{SSATTTS2017, title = {SMT Solving for Arithmetic Theories: Theory and Tool Support}, author = {Erika Ábrahám and Gereon Kremer}, publisher = {IEEE}, pages = {1-8}, type = {Conference Paper}, year = {2017}, doi = {10.1109/SYNASC.2017.00009}, url = { https://publications.rwth-aachen.de/record/780487}, }× [issue]	Erika Ábrahám, Gereon Kremer. SMT Solving for Arithmetic Theories: Theory and Tool Support, 19. International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2017), 1-8, IEEE, 2017.
2016
[bibtex] @conference{AGBBAIASMNIA2016, title = {A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic}, author = {Gereon Kremer and Florian Corzilius and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {9890}, pages = {315-335}, type = {Conference Paper}, year = {2016}, doi = {10.1007/978-3-319-45641-6_21}, url = { https://publications.rwth-aachen.de/record/670551}, }× [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, 315-335, Springer, 2016.
[bibtex] @conference{ZOFDOUSCT2016, title = {Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies}, author = {Erika Ábrahám and Florian Corzilius and Einar Broch Johnsen and Gereon Kremer and Jacopo Mauro}, publisher = {Springer}, booktitle = {LNCS}, volume = {9984}, pages = {229-245}, type = {Conference Paper}, year = {2016}, doi = {10.1007/978-3-319-47677-3_15}, url = { https://publications.rwth-aachen.de/record/681504}, }× [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: Theories, Tools, and Applications (SETTA 2016), Volume 9984 of LNCS, 229-245, Springer, 2016.
[bibtex] @conference{SCTA2016, title = {Satisfiability Checking: Theory and Applications}, author = {Erika Ábrahám and Gereon Kremer}, publisher = {Springer}, booktitle = {LNCS}, volume = {9763}, pages = {9-23}, type = {Conference Paper}, year = {2016}, doi = {10.1007/978-3-319-41591-8_2}, url = { https://publications.rwth-aachen.de/record/683011}, }× [issue]	Erika Ábrahám, Gereon Kremer. Satisfiability Checking: Theory and Applications, Software Engineering and Formal Methods : 14. International Conference (SEFM 2016), Volume 9763 of LNCS, 9-23, Springer, 2016.
2015
[bibtex] @conference{SROSCTSPSS2015, title = {SMT-RAT: an Open Source C++ Toolbox for Strategic and Parallel SMT Solving}, author = {Florian Corzilius and Gereon Kremer and Sebastian Junges and Stefan Schupp and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {9340}, pages = {360-368}, type = {Conference Paper}, year = {2015}, doi = {10.1007/978-3-319-24318-4_26}, url = { https://publications.rwth-aachen.de/record/561680}, }× [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 2015), Volume 9340 of LNCS, 360-368, Springer, 2015.