Software Validation and Verification (Cod. 660AA)

Announcements

The results of the written exam of February 3 are available here.

Timetable (see announcements for last-minute changes)

Tuesday	:	16.00 - 18.00 (room A1)
Wednesday	:	14.00 - 16.00 (room M1)
Friday	:	16.00 - 18.00 (room C1)

Course Outline

The aim of the course is to introduce techniques for verifying and validating software properties. After an introduction to various types of approaches, the course will focus in detail on model checking for different classes of properties, both linear time and branching time. During lectures, we will present theoretical results, techniques for modeling systems, and methods for specifying and verifying properties. The lectures will be interleaved with exercise sessions. The final part of the course will be based on introductory seminars on advanced research topics.

Syllabus

• Modelling Systems
  • Transition systems and program graphs
  • Modelling Concurrent Systems
• Linear Time Properties
  • Invariants, Safety, Liveness and Fairness
  • Checking regular safety properties
  • Checking omega regular properties with Büchi automata
• Linear Time Logics
  • Positive Normal Forms
  • Fairness
  • Model checking LTL formulas
• Branching Time Logics
  • Computational Tree Logics
  • Comparison of the expressivity of LTL, CTL and CTL*
  • Model checking CTL and CTL* formulas

Bibliography

The main reference for the course is the book Principles of Model Checking by Christel Baier and Joost-Pieter Katoen (please, keep into account the errata corrige). We will focus on chapters 1 to 6, and we will use the slides by Prof. Christel Baier and Prof. Joost-Pieter Katoen, which closely follow the book. We suggest the book Temporal Logic and State Systems by Fred Kröger and Stephan Merz as additional material for those who want more detailed explanation on temporal logic.

References for the advanced topics of the seminars will be given later during the course.

Exam

The exam consists of a written test on the topics of the syllabus, and a seminar on one of the advanced topics presented during the last part of the course.

Lessons

Module: Basics of Model Checking
• 16/09 -- Introduction to the course: Introduction slides, Modeling Sequential Systems slides.
• 17/09 -- True concurrency, Shared Variables, Synchronization: slides, Remarks on Operators slides.
• 19/09 -- Synchronous and Ansynchronous Message Passing with Channels: slides.
• 23/09 -- Exercise Session: Ex1 and Ex3 of exercise sheet.
• 24/09 -- Exercise Session: Ex2 and Ex4 of exercise sheet.
• 26/09 -- Linear Time Properties, State-based Linear Time View: slides.
• 30/09 -- Invariants and Safety Properties, Finite Trace and Trace Inclusion: slides.
• 01/10 -- Liveness Properties, Fairness Assumptions: slides.
• 03/10 -- Exercise Session: Ex3 and Ex4 of exercise sheet.
• 07/10 -- Exercise Session: Ex1 and Ex2 of exercise sheet.
• 08/10 -- Regular Safety Properties: slides.
• 14/10 -- ω-Regular Properties: slides.
• 15/10 -- Model checking ω-Regular Properties: slides.
• 17/10 -- Exercise Session: exercise sheet.
• 21/10 -- Exercise Session: exercise sheet.

Module: a Side Path on Some Program Analysis

• 22/10 -- Program Analysis : paper and slides.
• 28/10 -- Static and Dynamic Enforcement of Security Properties : slides.
• 29/10 -- Symbolic Execution : slides.
• 31/10 -- SMT: Satisfiability Modulo Theories : slides.
• 04/11 -- Symbolic Execution Formally Explained : slides.
• 05/11 -- Symbolic Execution: Challenges : slides.
• 07/11 -- Symbolic Semantics and Intermediate Representation : slides.

Module: Model Checking Temporal Logics

• 11/11 -- Syntax and Semantics of Linear Temporal Logic : slides.
• 12/11 -- Positive Normal Form of LTL and LTL modulo Fairness : slides.
• 14/11 -- Model Checking Linear Temporal Logic : slides.
• 18/11 -- Exercise Session: exercise sheet.
• 19/11 -- Exercise Session: exercise sheet.
• 21/11 -- Syntax and Semantics of Computation Tree Logic : slides.
• 25/11 -- Expressivity of CTL : slides.
• 26/11 -- Model Checking CTL : slides.
• 28/11 -- CTL with Fairness : slides.
• 02/12 -- CTL* : slides.
• 03/12 -- Exercise Session: exercise sheet.
• 05/12 -- Exercise Session: exercise sheet.

Towards Exams

• 09/12 -- Discussion of Advanced Topics for Seminars : slides.
• 10/12 -- Written Exam: exam -- results.
• 13/01 -- Written Exam: exam -- results.
• 03/02 -- Written Exam: exam -- results.