|Research Group Computer Science 2||Dept. of Computer Science|
Prof. Dr. Erika Ábrahám, Prof. Dr. Jürgen Giesl, Florian Frohn, David Korzeniewski, Jera Hensel, 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 will take place as a block seminar on the 24th of July 2017 from 9 am to 4 pm in our seminar room (4201b). We have a series of strict deadlines before that.
The initial meeting will take place on the 2nd of May 2017, 12:00, 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!
|24.07.17||9:00||Idil Esen Zulfikar||Prof. Dr. Erika Ábrahám||Minimal Infeasible Subset|
|9:45||Nicolas Jezuita||Jera Hensel||Answer Set Programming|
|10:30||Moritz Clever||Gereon Kremer||Difference Logic|
|11:15||Joel Charles||Gereon Kremer||Nelson Oppen Integration Scheme|
|13:00||Ömer Sali||Johanna Nellen||Interval Constraint Propagation|
|13:45||Mohammad Touhidur Rahman||Prof. Dr. Jürgen Giesl||SMT for Termination of LLVM|
|14:30||Marta Grobelna||Florian Frohn||Termination Analysis via MAX-SMT|
|15:15||Fabian Böller||David Korzeniewski||Compositional Safety via MAX-SMT|
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 David Korzeniewski.
|Disclaimer||Research Group Computer Science 2||Dept. of Computer Science|