RISC JKU

Logic-based Program Verification

NEWS!!!

General Presentation

The main objective of this lecture is to discuss decision procedures for various first-order theories.

First-order logic has proven to be a suitable formalism in various applications domains. Unfortunately, full first-order 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 first-order logics theories which appear in program verification and we will:

More precisely we plan to cover topics like:

  1. Propositional and first-order logic; first-order logic theories.
  2. Satisfiability checking in propositional logic.
  3. Satisfiability in first-order theories.
  4. Satisfiability checking in combination of theories.

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.

Organization

Winter Semester 2013.

Number:326.0LS
Title:Logic-based Program Verification
Lecturers:Madalina Erascu and Tudor Jebelean
Time:Wednesday, 8:30-10: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
Course outline (tentative)
Lecture 1 (BA9907) 09.10.2013
Motivation
Propositional logic
 
Syntax, semantics
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, set-of-support strategy, ordered resolution.
Lecture 7 20.11.2013
How to give talks (Slides)
First-Order Theories
 
Theory of Equality. Congruence Closure Algorithm for the quantifier-free fragment (Slides, Exercises)
Lecture 8 27.11.2013 No lecture
Lecture 9 to 14 04.12.2013-29.01.2014 Quantified Linear Arithmetic Quantifier Elimination over Integers, Quantifier Elimination over Rationals
Quantifier-Free Linear Arithmetic
Quantifier-Free Equality
Arrays
Interpolation
Lecture notes

Lecture notes (slides) will be available online after each lecture (except some lectures when you should take notes in order to prepare the homework).

Homeworks

There will be TWO assignments covering the first, respectively, second part of the lecture.

Presentation

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.

Grading

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%).