Exams
The exams will take place in the week March, 31st to April, 4th.- Please register by adding yourself to the list at our secretariate (building 052, 00-023)
- The dates are given out on a first come, first serve basis.
- Note: you also need to register at the Prüfungsamt!
If you cannot do the exam in this week, you have to make an appointment with Prof. Andreas Podelski and Dr. Jochen Hoenicke.
Instructors
Dates and Location
Lecture:
- Tue, 11 - 13h, SR 01-018 Geb. 101
- Thu, 10 - 11h, SR 01-018 Geb. 101
Tutorials:
- Jochen Hoenicke, Do 16:00, Treffpunkt: Geb. 52, 00-016
- Sergio Feo, Fr 16:00, Meeting point: Geb. 52, 00-016
Description
Decision Procedures are the basis for program verification: The task of program verification is to give a formal proof that a program meets its specification. This amounts to determining the truth value of a logical formula. A decision procedure is an algorithm that can for a certain type of formulas decide whether the formula is true or false.
We will investigate decision procedures for different logics. Starting with propositional logic we will investigate decision procedures for logics with integers, reals, recursive structures (lists and trees), arrays, etc.
Slides
- Lecture 1 (23 Oct 2007)
- Lecture 2 (25 Oct 2007)
- Lecture 3 (30 Oct 2007)
- Lecture 4 (6 Nov 2007)
- Lecture 5 (8 Nov 2007)
- Lecture 6 (13 Nov 2007)
- Lecture 7 (15 Nov 2007)
- Lecture 8 (20 Nov 2007)
- Lecture 9 (22 Nov 2007)
- Lecture 10 (27 Nov 2007)
- Lecture 11 (29 Nov 2007)
- Lecture 12 (4 Dec 2007)
- Lecture 13 (6 Dec 2007)
- Lecture 14 (13 Dec 2007)
- Lecture 15 (18 Dec 2007)
- Lecture 16 (20 Dec 2007)
- Lecture 17 (8 Jan 2008)
- Lecture 18 (10 Jan 2008)
- Lecture 19 (15 Jan 2008)
- Lecture 20 (17 Jan 2008)
- Lecture 21 (22 Jan 2008)
- Lecture 22 (24 Jan 2008)
- Lecture 23 (29 Jan 2008)
- Lecture 24 (31 Jan 2008)
- Lecture 25 (5 Feb 2008)
- Lecture 26 (7 Feb 2008)
- Lecture 27 (11-13 Feb 2008)
Exercise
- Exercise 1 (25 Oct 2007)
- Exercise 2 (1 Nov 2007)
- Exercise 3 (8 Nov 2007)
- Exercise 4 (15 Nov 2007)
- Exercise 5 (22 Nov 2007)
- Exercise 6 (29 Nov 2007)
- Exercise 7 (6 Dec 2007)
- Exercise 8 (14 Dec 2007)
- Exercise 9 (10 Jan 2008)
- Exercise 10 (17 Jan 2008)
- Exercise 11 (24 Jan 2008)
- Exercise 12 (31 Jan 2008)
- Exercise 13 (7 Feb 2008)
piVC (πVC)
Binaries for MacOS X and Linux and sources for πVC can be downloaded from Aaron Bradley's Homepage. I have built binaries for Cygwin (extract it into C:\pivc). Yices can be downloaded from the yices web-site.
Links & Literature
- A.R. Bradley, Z. Manna: The Calculus of Computation, Springer, 2007
- H. Arnold: A linearized DPLL calculus with learning
- S. Krstić: Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL, Materials of Dagstuhl Seminar Deduction and Decision Procedures, 2007