Florian Corzilius

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

Research

  • (Non)linear real and integer arithmetic
  • SMT solving
  • Virtual substitution method
  • Simplex
  • Interval constraint propagation

Research

An open source C++ toolbox for strategic and parallel SMT solving.
Available at:
https://github.com/smtrat/smtrat/wiki
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 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 fulltext PDF [bibtex] [issue] Christian Dehnert, Erika Ábrahám, Florian Corzilius, Harold Yorick Bruintjes, Joost-Pieter Katoen, Matthias Volk, Nils Jansen, Sebastian Junges. Parameter synthesis for probabilistic systems, 19. GI/ITG/GMM-Workshop "Methoden und Beschreibungsprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV 2016), 72-74, Albert-Ludwigs-Universität, 2016.
DOI fulltext PDF [bibtex] [issue] Florian Corzilius. Integrating virtual substitution into strategic SMT solving, PhD Thesis, RWTH Aachen University, 1 Online-Ressource (IX, 186 Seiten) : Illustrationen, Diagramme, 2016.
2015
DOI [bibtex] [issue] Erika Ábrahám, Florian Corzilius, Hans Christian Dehnert, Harold Yorick Bruintjes, Joost-Pieter Katoen, Matthias Volk, Nils Jansen, Sebastian Junges. PROPhESY, International Conference on Computer Aided Verification (CAV'15), Volume 9206 of LNCS, 214-231, Springer, 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.
2014
DOI [bibtex] [issue] Bernd Becker, Erika Ábrahám, Florian Corzilius, Joost-Pieter Katoen, Matthias Volk, Nils Jansen, Ralf Wimmer. Accelerating Parametric Probabilistic Verification, 11th International Conference on Quantitative Evaluation of Systems (QEST 2014), Volume 8657 of LNCS, 404-420, Springer, 2014.
2013
DOI [bibtex] [issue] Bernd Becker, Erika Ábrahám, Florian Corzilius, Karsten Scheibler, Ulrich Loup. A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition, Volume 7898 of LNCS, 193-207, Springer, 2013.
DOI [bibtex] [issue] Erika Ábrahám, Florian Corzilius, Sebastian Junges, Ulrich Loup. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers, Volume 8080 of LNCS, 186-198, Springer, 2013.
fulltext PDF [bibtex] [issue] Erika Ábrahám, Florian Corzilius, Sebastian Junges, Ulrich Loup. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers, Volume 2013,08 of Aachener Informatik-Berichte : AIB, 3-21, Shaker [u.a.], 2013.
arXiv:1312.3979 [bibtex] [issue] Bernd Becker, Erika Ábrahám, Florian Corzilius, Joost-Pieter Katoen, Matthias Volk, Nils Jansen, Ralf Wimmer. Accelerating Parametric Probabilistic Verification, 21 Seiten, 2013. https://arxiv.org/abs/1312.3979
2011
DOI [bibtex] [issue] Erika Ábrahám, Florian Corzilius. Virtual Substitution for SMT-Solving, Fundamentals of computation theory (FCT 2011), Volume 6914 of LNCS, 360-371, Springer, 2011.
[bibtex] [issue] Florian Corzilius, Johanna Nellen, Nadine Bergner, Nils Jansen, Philipp Brauner, Thiemo Leonhardt, Ulrich Loup, Ulrik Schroeder. On collaboratively conveying computer science to pupils, 11th Koli Calling International Conference on Computing Education Research (KOLI'11), 132-137, ACM, 2011.