|Research Group Computer Science 2||Dept. of Computer Science|
Prof. Dr. Erika Ábrahám, Prof. Dr. Jürgen Giesl, Cornelius Aschermann, Florian Corzilius, Florian Frohn, Jera Hensel, Gereon Kremer, Johanna Nellen, Stefan Schupp, Thomas Ströder
The focus of this seminar is automatic satisfiability checking of formulae. Here we consider several logics, e.g., pure propositional logic, but also extensions like quantified boolean formulae or SAT modulo theories. We will discuss both techniques for efficient satisfiability checking and practical applications in program verification.
The seminar will take place on the 30th and 31st of July 2015 in our seminar room (4201b). We have a series of strict deadlines before that.
The initial meeting will take place on the 30th of April, 4pm, in our seminar room (4201b).
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!
|30.07.15||09:30||Todorov, Georgi||Prof. Dr. Jürgen Giesl||Introduction to SAT and SMT via the DPLL Algorithm|
|10:15||Hans, Christian||Gereon Kremer||Incremental SAT|
|11:00||Neuberger, Lukas||Stefan Schupp||Interval Constraint Propagation|
|11:45||Hütter, Dustin||Gereon Kremer and Stefan Schupp||SMT-NIA via SMT-LIA|
|13:15||Müller, Norman||Florian Corzilius||Nonlinear Real Arithmetic via Sum of Squares|
|14:00||Casatchina, Elena||Prof. Dr. Erika Ábrahám and Florian Corzilius||Quantified Boolean Formulas|
|14:45||Haps, Kim||Prof. Dr. Erika Ábrahám||Bitvectors|
|31.07.15||09:30||Hermanns, Judith||Jera Hensel||Program Analysis via Constraint Solving|
|10:15||Neuss, Malte||Prof. Dr. Jürgen Giesl||Termination Analysis via MAX-SAT|
|11:00||Pago, Benedikt||Thomas Ströder||Nontermination Analysis via Symbolic Execution and SMT|
|11:45||Karaca, Bugra||Thomas Ströder||Synthesizing shortest XOR circuits using SAT|
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.
If you want to use subversion for your paper and / or slides, please contact Gereon Kremer.
For further details please contact Florian Frohn.
|Disclaimer||Research Group Computer Science 2||Dept. of Computer Science|