Personal Info about Florian Corzilius


I'm a PHD student in the Hybrid Systems Group led by Prof. Erika Ábrahám.

 

E-Mail: corzilius@cs.rwth-aachen.de

Phone: +49-241/80-21243

Fax: +49-241/80-22243

Visiting Address

Room 4228

Ahornstraße 55

52074 Aachen

 

 


Research

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


Maintained software projects

SMT-RAT — The Satisfiability–Modulo–Theories Real Arithmetic Toolbox


    An open-source C++ toolbox offering theory solver modules for the development of SMT solvers for nonlinear real arithmetic (NRA).

    Available at:
    http://smtrat.sourceforge.net/


    Teaching Assistance

    Sommer 2013

    Winter 2012/2013

    Sommer 2012

    Winter 2011/2012

    Sommer 2011


    Publications

    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.
    DownloadFlorian 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.
    DownloadFlorian Corzilius. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers, Talk at 5th International Conference on Algebraic Informatics, 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. Virtual Substitution in SMT Solving. Diploma thesis at RWTH Aachen, 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. A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra. 8th Int. Workshop on Satisfiability Modulo Theories (SMT'10), 2010.
    DownloadErika Abraham, Ulrich Loup, Florian Corzilius, Thomas Sturm. A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra,. Verification over Discrete-Continuous Boundaries, Dagstuhl Seminar, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2010.
    2011
    DownloadFlorian Corzilius. Virtual Substitution in SMT Solving. Diploma thesis at RWTH Aachen, 2011.



    Selected Talks