NEWS!!!
The main objective of this lecture is to discuss decision procedures for various firstorder theories.
Firstorder logic has proven to be a suitable formalism in various applications domains. Unfortunately, full firstorder logic (FOL) is undecidable. Fortunately, in applications, it is often the case that only fragments of FOL appear, which are decidable and sometimes even have a low complexity. Decidable theories are, e.g., Presburger arithmetic, theory of reals, certain fragments of theories of data structures such as lists, pointers and arrays.
In this lecture, we will consider firstorder logics theories which appear in program verification and we will:
More precisely we plan to cover topics like:
The seminar is mainly based on the book "The Calculus of Computation" by Aaron R. Bradley and Zohar Manna.
The lecture consists in two parts. The first part is presented by us. From the second part, each student has to choose one topic and present it in the lecture. The presentation counts in high amount to the final grade.
The purpose of the first part of Lecture 7 is to prepare the students for the presentation.
Winter Semester 2013.
Number:  326.0LS 
Title:  Logicbased Program Verification 
Lecturers:  Madalina Erascu and Tudor Jebelean 
Time:  Wednesday, 8:3010:00 
Room:  S2 054, except 09.10, 16.10, 23.10, 30.10, 06.11, 13.11 when we will meet in BA9907 
Language:  English 
First meeting:  October 9 
Registration:  Via the KUSSS system. 
Office hours:  By appointment 
Lecture 1 (BA9907)  09.10.2013 



Lecture 2 (BA9907)  16.10.2013  Propositional Logic  Equivalence, rewriting, normal forms; the resolution principle for propositional logic, correctness and completeness  
Lecture 3 (BA9907)  23.10.2013  Predicate Logic (Slides, Exercises)  The syntax of first order predicate logic: terms and formulas; the semantics of first order predicate logic: interpretations; computing the truth value; equivalences of quantified formulae; normal forms: prenex, Skolem, standard.  
Lecture 4 & 5 (BA9907)  30.10.2013, 06.11.2013  Predicate Logic (Slides, Exercises)  Substitutions, unification. The resolution principle for predicate logic, correctness and completeness.  
Lecture 6 (BA9907)  13.11.2013  Propositional & Predicate Logic  The DPLL method for SAT solving; Resolution strategies: hyperresolution, setofsupport strategy, ordered resolution.  
Lecture 7  20.11.2013 



Lecture 8  27.11.2013  No lecture  
Lecture 9 to 14  04.12.201329.01.2014  Quantified Linear Arithmetic  Quantifier Elimination over Integers, Quantifier Elimination over Rationals  
QuantifierFree Linear Arithmetic  
QuantifierFree Equality  
Arrays  
Interpolation 
Lecture notes (slides) will be available online after each lecture (except some lectures when you should take notes in order to prepare the homework).
There will be TWO assignments covering the first, respectively, second part of the lecture.
Each student is supposed to prepare a presentation covering the topics from the second part. You should choose your presentation topic by end October/mid November. You should contact us two times before the presentation to discuss the contents of it.
There will be no final exam. Your course grade will be based on your active presence in the lectures (10%), the homeworks (30%) and the presentation (60%).