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 fulltext PDF [bibtex] 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.
DOI fulltext PDF [bibtex] Florian Corzilius. Integrating virtual substitution into strategic SMT solving, PhD Thesis, RWTH Aachen University, 186 pages, 2016.
DOI fulltext PDF [bibtex] Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám. Parameter synthesis for probabilistic systems, 19. GI/ITG/GMM-Workshop "Methoden und Beschreibungsprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV 2016), pages 72-74, Albert-Ludwigs-Universität, 2016.
DOI [bibtex] 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, pages 229-245, Springer, 2016.
2015
DOI [bibtex] Hans Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám. PROPhESY : A PRObabilistic ParamEter SYnthesis Tool, International Conference on Computer Aided Verification (CAV'15), Volume 9206 of LNCS, pages 214-231, Springer, 2015.
DOI [bibtex] 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, pages 360-368, Springer, 2015.
2014
DOI [bibtex] Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification, 11th International Conference on Quantitative Evaluation of Systems (QEST 2014), Volume 8657 of LNCS, pages 404-420, Springer, 2014.
2013
arXiv:1312.3979 [bibtex] Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification, 2013. arXiv:1312.3979
fulltext PDF [bibtex] Sebastian Junges, Ulrich Loup, Florian Corzilius, Erika Ábrahám. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers, Volume 2013,08 of Aachener Informatik-Berichte : AIB, pages 3-21, Shaker [u.a.], 2013.
DOI [bibtex] Sebastian Junges, Ulrich Loup, Florian Corzilius, Erika Ábrahám. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers, Algebraic informatics (CAI 2013), Volume 8080 of LNCS, pages 186-198, Springer, 2013.
DOI [bibtex] Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika Ábrahám, Bernd Becker. A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition, Automated Deduction, Volume 7898 of LNCS, pages 193-207, Springer, 2013.
2012
DOI [bibtex] Florian Corzilius, Ulrich Loup, Sebastian Junges, Erika Ábrahám. SMT-RAT : An SMT-Compliant Nonlinear Real Arithmetic Toolbox, Theory and applications of satisfiability testing, Volume 7317 of LNCS, pages 442-448, Springer, 2012.
2011
[bibtex] Nadine Bergner, Philipp Brauner, Florian Corzilius, Nils Jansen, Thiemo Leonhardt, Ulrich Loup, Johanna Nellen, Ulrik Schroeder. On collaboratively conveying computer science to pupils, 11th Koli Calling International Conference on Computing Education Research (KOLI'11), pages 132-137, ACM, 2011.
DOI [bibtex] Florian Corzilius, Erika Ábrahám. Virtual Substitution for SMT-Solving, Fundamentals of computation theory (FCT 2011), Volume 6914 of LNCS, pages 360-371, Springer, 2011.
2010
fulltext PDF [bibtex] Erika Ábrahám, Ulrich Loup, Florian Corzilius, Thomas Sturm. SMT-Solving in the Analysis and Synthesis of Hybrid Systems, Verification over discrete-continuous boundaries, Volume 10271 of Dagstuhl Seminar Proceedings, pages 9 S., Schloss Dagstuhl, Leibniz-Zentrum für Informatik, 2010.