|Research Group Computer Science 2||Dept. of Computer Science|
Prof. Dr. Erika Ábrahám, Prof. Dr. Jürgen Giesl, Florian Corzilius, Florian Frohn, David Korzeniewski, Gereon Kremer, Johanna Nellen, Stefan Schupp
The focus of this seminar is automatic satisfiability checking of formulas. Here we consider several logics, e.g., pure propositional logic, but also extensions like quantified boolean formulas or SAT modulo theories. We will discuss both techniques for efficient satisfiability checking and practical applications in program verification.
The seminar takes place on the 25th (E3, room 9u09) and 26th (E3, room 9222) of August 2016. We have a series of strict deadlines before that.
Your seminar paper should have 10 pages and be written in either English or German. Do not provide an index or table of contents, but attach a list of references. More than 5 spelling or grammar mistakes on a single page will lead to an immediate rejection of your paper, so please use an automated spell checker!
|25.08.16||09:30||Böhr, Nico||David Korzeniewski||Introduction to SAT and SMT via the DPLL Algorithm|
|10:15||Sabau, Alex||Gereon Kremer||Symmetry Breaking|
|11:00||Gerasimov, Arkadii||Gereon Kremer||Nelson Oppen Integration Scheme|
|11:45||Ilov, Petyo||Prof. Dr. Erika Ábrahám||Omega-Test|
|13:15||Srecec, Stefan||Stefan Schupp||SMT-NIA via SMT-LIA|
|14:00||Winkler, Tobias||Florian Corzilius||Polyhedral Approximation of NRA|
|26.08.16||09:30||Nehring-Wirxel, Julius||Florian Frohn||Synthesis of Polynomial Interpretations|
|10:15||Kruse, Sebastian||Prof. Dr. Jürgen Giesl||SMT for Termination of LLVM|
|11:00||Frerich, Kai||Prof. Dr. Jürgen Giesl||Termination Analysis via MAX-SMT|
|11:45||Penners, Ralf||David Korzeniewski||Compositional Safety via MAX-SMT|
|13:15||Sanka, Klea||Prof. Dr. Erika Ábrahám||Bounded Model Checking|
|14:00||Kraeutmann, David||Florian Frohn||Integration of SMT to Coq|
The talks should not take more than 25 minutes and can be held in either English or German.
You can find templates for your paper here. Using them is optional.
For further details please contact Florian Frohn.
|Disclaimer||Research Group Computer Science 2||Dept. of Computer Science|