Florian Corzilius | Theory of Hybrid Systems

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
[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{P2016, title = {Parameter synthesis for probabilistic systems}, author = {Hans Christian Dehnert and Sebastian Junges and Nils Jansen and Florian Corzilius and Matthias Volk and Harold Yorick Bruintjes and Joost-Pieter Katoen and Erika Ábrahám}, publisher = {Albert-Ludwigs-Universität}, pages = {72-74}, type = {Conference Paper}, year = {2016}, doi = {10.6094/UNIFR/10639}, url = { https://publications.rwth-aachen.de/record/683021}, }× [issue]	Hans 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), 72-74, Albert-Ludwigs-Universität, 2016.
[bibtex] @phdthesis{IS2016, title = {Integrating virtual substitution into strategic SMT solving}, author = {Florian Corzilius}, institution = {RWTH Aachen University}, pages = {1 Online-Ressource (IX, 186 Seiten) : Illustrationen, Diagramme}, type = {PhD Thesis}, year = {2016}, doi = {10.18154/RWTH-2017-03775}, url = { https://publications.rwth-aachen.de/record/688379}, }× [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
[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.
[bibtex] @conference{PAPPST2015, title = {PROPhESY: A PRObabilistic ParamEter SYnthesis Tool}, author = {Hans Christian Dehnert and Sebastian Junges and Nils Jansen and Florian Corzilius and Matthias Volk and Harold Yorick Bruintjes and Joost-Pieter Katoen and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {9206}, pages = {214-231}, type = {Conference Paper}, year = {2015}, doi = {10.1007/978-3-319-21690-4_13}, url = { https://publications.rwth-aachen.de/record/564236}, }× [issue]	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, 214-231, Springer, 2015.
2014
[bibtex] @conference{APPV2014, title = {Accelerating Parametric Probabilistic Verification}, author = {Nils Jansen and Florian Corzilius and Matthias Volk and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker}, publisher = {Springer}, booktitle = {LNCS}, volume = {8657}, pages = {404-420}, type = {Conference Paper}, year = {2014}, doi = {10.1007/978-3-319-10696-0_31}, url = { https://publications.rwth-aachen.de/record/540007}, }× [issue]	Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification, 11. International Conference on Quantitative Evaluation of Systems (QEST 2014), Volume 8657 of LNCS, 404-420, Springer, 2014.
2013
[bibtex] @conference{ASICPCAD2013, title = {A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition}, author = {Ulrich Loup and Karsten Scheibler and Florian Corzilius and Erika Ábrahám and Bernd Becker}, publisher = {Springer}, booktitle = {LNCS}, volume = {7898}, pages = {193-207}, type = {Conference Paper}, year = {2013}, doi = {10.1007/978-3-642-38574-2_13}, url = { https://publications.rwth-aachen.de/record/207654}, }× [issue]	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, 193-207, Springer, 2013.
[bibtex] @conference{OGBCSMTSRN2013, title = {On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers}, author = {Sebastian Junges and Ulrich Loup and Florian Corzilius and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {8080}, pages = {186-198}, type = {Conference Paper}, year = {2013}, doi = {10.1007/978-3-642-40663-8_18}, url = { https://publications.rwth-aachen.de/record/226897}, }× [issue]	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 : 5. international conference (CAI 2013), Volume 8080 of LNCS, 186-198, Springer, 2013.
[bibtex] @techreport{OGBCSMTSRN2013, title = {On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers}, author = {Sebastian Junges and Ulrich Loup and Florian Corzilius and Erika Ábrahám}, publisher = {Shaker [u.a.]}, booktitle = {Aachener Informatik-Berichte : AIB}, volume = {2013,08}, pages = {3-21}, type = {Tech Report}, year = {2013}, url = { https://publications.rwth-aachen.de/record/228582}, }× [issue]	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, 3-21, Shaker [u.a.], 2013.
[bibtex] @unpublished{APPV2013, title = {Accelerating Parametric Probabilistic Verification}, author = {Nils Jansen and Florian Corzilius and Matthias Volk and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker}, pages = {21 Seiten}, type = {Preprint}, year = {2013}, url = { https://arxiv.org/abs/1312.3979}, }× [issue]	Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification, 21 Seiten, 2013. https://arxiv.org/abs/1312.3979
2011
[bibtex] @conference{VSSS2011, title = {Virtual Substitution for SMT-Solving}, author = {Florian Corzilius and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {6914}, pages = {360-371}, type = {Conference Paper}, year = {2011}, doi = {10.1007/978-3-642-22953-4_31}, url = { https://publications.rwth-aachen.de/record/116784}, }× [issue]	Florian Corzilius, Erika Ábrahám. Virtual Substitution for SMT-Solving, Fundamentals of computation theory:18th international symposium, FCT 2011 (FCT 2011), Volume 6914 of LNCS, 360-371, Springer, 2011.
[bibtex] @conference{O2011, title = {On collaboratively conveying computer science to pupils}, author = {Nadine Bergner and Philipp Brauner and Florian Corzilius and Nils Jansen and Thiemo Leonhardt and Ulrich Loup and Johanna Nellen and Ulrik Schroeder}, publisher = {ACM}, pages = {132-137}, type = {Conference Paper}, year = {2011}, url = { https://publications.rwth-aachen.de/record/118012}, }× [issue]	Nadine Bergner, Philipp Brauner, Florian Corzilius, Nils Jansen, Thiemo Leonhardt, Ulrich Loup, Johanna Nellen, Ulrik Schroeder. On collaboratively conveying computer science to pupils, 11. Koli Calling International Conference on Computing Education Research (KOLI'11), 132-137, ACM, 2011.