|Research Group Computer Science 2||Dept. of Computer Science|
Prof. Dr. Erika Ábrahám, Prof. Dr. Jürgen Giesl, Stefan Dollase, Marcel Hark, Jera Hensel, Rebecca Haehn, Gereon Kremer,
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 (e.g., in July 2019). The preliminary discussion took place on April 4, 2019 at 10:30 in 5055.
The seminar will take place on the as a block seminar on August 1st 2019. We have a series of strict deadlines before that.
Your seminar paper should have 10 pages in a format similar to the template given below. It can 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!
|Linear Optimization via SMT||Link||Rebecca Haehn||Dennis Prudlik|
|Verification of Neural Networks||Link||Prof. Dr. Erika Ábrahám||David Klüner|
|Termination of Triangular Integer Loops is Decidable||N.N.||Prof. Dr. Jürgen Giesl||Eric Skaliks|
|Proving termination of imperative programs using Max-SMT||Link||Stefan Dollase||Kai Liehr|
|Answer Set Programming Based on Propositional Satisfiability||Link||Jera Hensel||Dinh-An Ho|
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 Marcel Hark.
|Disclaimer||Research Group Computer Science 2||Dept. of Computer Science|