Systems Verification Lab

  • The page of the same course held in Academic Year 2019/2020 can be found at this link.
  • 28/09/2020: The course page is online. The course will be held in the second semester (from 1st March 2021).


ESSE3 Link

Lectures schedule:

  • From March 3rd 2021 - Wednesdays from 2.00pm to 4.00pm - Fridays from 11.00am to 1.00pm

Recording of Lectures and other material:

Webex Room for Lecture Streaming

Office hours:

  • Take an appointment with the teacher via email. Office hours can be online (webex) or in presence.


  • The course official acronym is SVL2021

See ESSE3 link.

See ESSE3 link.

Verification Tools

Reactive Systems

Transition Systems and Modelling Languages for Reactive Systems

Linear Time Properties

Linear Time Logic (LTL)

Computation Tree Logic (CTL)

Timed Systems

Timed Automata


Exercises with (some) solutions

  • Regular Properties, LTL and CTL - NOTE 1: some of the exercises on Regular Properties and on LTL require to calculate the product between the transition system and the non-Deterministic Buechi Automaton (NBA) corresponding to the formula - ignore that part and justify your answer by providing the counterexample without providing the product construction. NOTE 2: some of the exercises on CTL require to show the steps of the Sat algorithm for deciding the satisfaction of the formula by a state or by a transition system: ignore this request and provide, if possible, an informal justification; if not possible ignore the exercise.

Sample Past Written Tests with Solutions


  • Christel Baier, Joost-Pieter Katoen, “Principles of Model Checking”, The MIT Press, 2008.

Reference books

  • Michael Huth, Mark Ryan, “Logic in Computer Science”, Second Edition, Cambridge University Press, 2004. ISBN: 9780521543101.
  • Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, Jiri Srba, “Reactive Systems”, Cambridge University Press, 2007.

Exam Dates A.Y. 2020/2021

Dates of Partial Exams “SVL2021 Sess. XXX - Project Delivery” and “SVL2021 Sess. XXX - Written Test” can be found in the ESSE3 Career System after login.

Exam rules

The exam consists of a written test, containing open-answer questions, together with one project, realised with the tools introduced in the course (see section “Projects” above). The Written Test and the Project are two independent Partial Exams (see the exam sessions in the ESSE3 career system) and can be passed in different exam sessions. The final grade, which is the average of the grades of the two Partial Exams, can be obtained and registered only if both the Partial Exams have been passed with a grade of at least 18/30.

Registration for the written tests must be done using the Student Career System ESSE3 here. Please note that the registration deadline is usually 3 working days before the written test date. During the exercise sessions throughout the course samples of the written test questions will be presented with solutions. During the written test students can consult a hand-written A4 paper of their production for reference.

Instructions for Sending Projects

Students must create a folder in Google Drive, using the Google account associated to their email

The folder must contain all the files relative to the project and a written report, in English, which describes all the phases of the developing of the project. The use of screenshots is encouraged to show, within the report, the runs and the results of the project.

The folder must be named


where N is the number of the realised project (according to the section “Projects” above) and X is the number of the exam session (Appello) as specified for each date of the written test above.

The folder must be shared (using Google Drive facilities) with and by 11.59pm of the day before the written test scheduled for the selected session X.

Students that send the project must also register to the Partial Exam “SVL2021 Sess. XXX - Project Delivery” in ESSE3, specified for each exam session.

Exam Results

  • The results will be communicated through this site or by email (depending on the number of students).
  • Contextually to the communication of the results, students will be invited to accept or reject the evaluation.
  • A positive evaluation (>=18/30) of each Partial Exam (Written Test and Project) remains valid for one year or until the student retries the Partial Exam.
  • If both grades (Written Test and Project) are accepted, the final grade will be registered in ESSE3.