42005 - Deduction and Verification Techniques (TDV)

 

 

 

The aim of this course is to present the state of the art in automatic and semi-automatic deduction and verification. Showing the currently used techniques as well as the existing running tools and its industrial applications.

1. Deduction in first-order logic (FOL) with equality. Rewriting techniques. Paramodulation.
2. Model checking. Temporal logic. Properties. Algorithms. Symbolic model checking. Existing tools.
3. Abstract interpretation. Abstractions, approximations and fix points. Applications to program static analysis.
4. Higher-order logics. Lambda calculus. Proof asistants: Functionalities and use. Examples: HOL, Isabelle, PVS, Coq (only some of these systems will be presented). Application of HOL to circuit verification in Intel.

The 6 ECTS of this subject are divided in different types of activities: lectures on theory and problems (TP), laboratory lessons (LAB), studying and solving problems with notes, articles and book chapters and exercise lists (EST), an implementation project (IMP) and an evaluation test (AVAL).
TP lectures will introduce fundamental concepts and the solutions of proposed problems will be revised.
At LAB lessons, practical problem resolution exercises will be proposed, using different tools.

Evaluation will take into account the different activities done along the course.
At the end of the course, there will be a written exam that basically consists of solving problems similar to those done in the course.
Implementation projects must be handed out in class to the teacher. Students will have to explain them and answer the teacher’s questions.



Rooms with terminal for laboratories (1 hour per week). Materials prepared by the teacher will be available for students (copies of manuscript notes or of transparencies used in class, and exercise lists).