Florian Corzilius

corzilius

Email
corzilius at cs.rwth-aachen.de
Phone
+49 (0)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

Publications for Florian Corzilius

2016
DownloadGereon 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.
DOIChristian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Joost-Pieter Katoen, Erika Abraham, Harold Bruintjes. Parameter Synthesis for Probabilistic Systems. Proc. of the 19th GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'16), pages 72-74, Albert-Ludwigs-Universität Freiburg, 2016.
Florian Corzilius. Integrating Virtual Substitution into Strategic SMT Solving. Phd Thesis at RWTH Aachen University, 2016.
DownloadErika 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
DOIFlorian 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.
DownloadChristian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Bruintjes, Joost-Pieter Katoen, Erika Abraham. PROPhESY: A PRObabilistic ParamEter SYnthesis Tool. Proc. of the 27th Int. Conf. on Computer Aided Verification (CAV'15), Volume 9206 of LNCS, pages 214–231, Springer, 2015.
2014
DownloadNils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification. 11th Int. Conf. on Quantitative Evaluation of Systems (QEST'14), Volume 8657 of LNCS, pages 404–420, Springer, 2014.
2013
DownloadNils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification. Technical report at Cornell University number arXiv:1312.3979, 2013.
DownloadSebastian Junges, Ulrich Loup, Florian Corzilius, Erika Abraham. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers. Proc. of the 5th International Conference on Algebraic Informatics (CAI'13), Volume 8080 of LNCS, pages 186–198, Springer-Verlag, 2013.
DownloadSebastian Junges, Ulrich Loup, Florian Corzilius, Erika Abraham. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers. Technical report at RWTH Aachen University number AIB-2013-08, 2013.
DownloadUlrich Loup, Karsten Scheibler, Florian Corzilius, Erika Abraham, Bernd Becker. A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition. Proc. of the 24th International Conference on Automated Deduction (CADE-24), Volume 7898 of LNCS, pages 193–207, Springer-Verlag, 2013.
2012
DownloadFlorian Corzilius, Ulrich Loup, Sebastian Junges, Erika Abraham. SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox (Tool Presentation). Int. Conf. on Theory and Applications of Satisfiability Testing (SAT'12), Volume 7317 of LNCS, pages 442–448, Springer Berlin Heidelberg, 2012.
2011
DownloadErika Abraham, Nadine Bergner, Philipp Brauner, Florian Corzilius, Nils Jansen, Thiemo Leonhardt, Ulrich Loup, Johanna Nellen, Ulrik Schroeder. On Collaboratively Conveying Computer Science to Pupils. Proc. of the 11th Koli Calling Int. Conf. on Computing Education Research (KOLI'11), pages 132–137, ACM, 2011.
DownloadFlorian Corzilius, Erika Abraham. Virtual Substitution for SMT Solving. 18th Int. Symp. on Fundamentals of Computation Theory (FCT'11), Volume 6914 of LNCS, pages 360–371, Springer Berlin Heidelberg, 2011.
2010
DownloadErika Abraham, Ulrich Loup, Florian Corzilius, Thomas Sturm. SMT-Solving in the Analysis and Synthesis of Hybrid Systems. Verification over Discrete-Continuous Boundaries, Dagstuhl Seminar, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2010.

Selected Talks

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.
Florian Corzilius. SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving, Talk at Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT'15), 2015.
2013
Florian Corzilius. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers, Talk at the 5th International Conference on Algebraic Informatics (CAI'13), 2013.
2011
DownloadFlorian Corzilius. Virtual Substitution for SMT Solving, Talk at In 18th Int. Symp. on Fundamentals of Computation Theory (FCT), 2011.
2010
Florian Corzilius. A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra, Talk at SMT 2010, 2010.