Decision Procedures


Preparatory Meeting: Tuesday, April 14, 2015: 10 - 12h, room 630 (Building E1 5)

Talks: Friday, June 19, 2015: 08:30 h, room 630 (Building E1 5)

Sample Topics

Congruence Closure, CDCL, Quantifier Elimination, Fourier-Motzkin, Simplex, Virtual Subsitution, SMT, Superposition, IC3


There are currently more applications than slots. Therefore, please have a look at the following paper which is one of the slots and which is a representative paper. The task is to turn it into to a talk that Presburger for the existential fragment is decidable and NP-complete. We expect you to be able to extract and understand the necessary information from the paper on your own. Please only register if you feel comfortable with such a task. If you already registered and don't feel comfortable with such a task, please ask Jennifer Müller ( to remove you from the list.

Representative Paper: ScarpelliniComplexityPresburger84.pdf


Register here for this course.
Don't forget to register with HISPOS since we are unable to do this automatically.

Registration is on a first come first serve basis.