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]
@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.
DOI [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.
DOI fulltext PDF [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.
DOI fulltext PDF [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
DOI [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.
DOI [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.
Show all