Software Validation and Verification (Cod. 660AA)

Announcements

January the 20th Dario Bekic will present the paper "Abstract Separation Logic" by Calcagno, at 16.00 in Sala Seminari Ovest, CS Department.

The results of the written exam of Jenuary the 13th are available here.

The results of the written exam of December the 10th are available here.

December the 9th we will discuss the proposed papers for the seminars (room A1, also online via Google Meet)

December the 10th there will be the pre-appello of the written exam of the course (room M1 -- the exam starts at 14.00!)

The lesson of Tuesday, November the 11th, will be in Sala Gerace (department of Computer Science)!

The lesson scheduled for Friday, October the 24th, will not be held!

The lesson scheduled for Friday, October 10th is cancelled due to UniPiOrienta2025!

The course will start on September 16th in room A1.

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.