VAI ALLA VERSIONE ITALIANA

OTHER ACADEMIC YEARS

Index:

Exams

Course programme

Textbooks

Class material

Class timetable

Software

Exams

Exams Rules

Please check lesson 1.

Project

Exams Dates

N	Date	Hour	Where	Notes	Deadline
1	approx 01/2027
2	approx 02/2027
3	approx 02/2027
4	approx 06/2027
5	approx 07/2027
6	approx 07/2027
7	approx 09/2027
straord	approx 11/2027

Course Programme

Introduction to Verification

• verification problem
• testing, model checking and other methodologies

Model Checking for Finite State Systems

• Murphi, SPIN and NuSMV
• CTL and LTL
• model checking algorithms: theoretical, explicit, symbolic, bounded model checking

Testing

• main techniques: functyional and structural testing
• testing within software development process: unit, integration, regression and system testing
• JUnit

Validation

• acceptance testing

Textbooks:

• Gerald Everett, Raymond McLeod Jr.: Software Testing: Testing Across the Entire Software Development Life Cycle, Wiley
• A version of this book is available in the library
• Mauro Pezzé, Michal Young: Software Testing and Analysis: Process, Principles, and Techniques, Wiley
• A version of this book is available here
• Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem (Editors): Handbook of Model Checking, Springer
• A version of this book is available here
• Christel Baier, Joost-Pieter Katoen: Principles of Model Checking, MIT Press
• A version of this book is available here

Class Material

N	Date	Material	Arguments	Notes
1	24/09/2026	slides	Introduction to testing, validation and verification of software systems	Slides 1-51
	25/09/2026		CANCELED
	01/10/2026		CANCELED
2	02/10/2026	slides Murphi models	The Murphi model checker: input language and usage	Lesson 1: slides 52-end. Lesson 2: Slides 1-end
3	08/10/2026	slides	The Murphi model checker: verification algorithm (part 1)	Slides 1-37
4	09/10/2026	See slides in lesson 3	The Murphi model checker: verification algorithm (part 2)	Slides 38-end
5	15/10/2026	slides	Safety e liveness properties. LTL	1-29
6	16/10/2026	slides	CTL semantics and CTL Model Checking algorithms	Lesson 5: Slides 30-end. Lesson 6: Slide 1-28
7	22/10/2026	slides	LTL Model Checking algorithm. SPIN and Promela (part 1)	Lesson 6: Slides 29-end. Lesson 7: Slide 1-35
8	23/10/2026	See slides in lesson 7	SPIN and Promela (part 2)	Slides 36-55
9	29/10/2026	slides	SPIN and Promela (part 3). NuSMV (part 1: OBDDs)	Lesson 7: Slides 55-end. Lesson 9: Slide 1-7
10	30/10/2026	See slides in lesson 9	NuSMV (part 2: input language)	Slides 8-56

Class Timetable

Day	From	To	Where
Thursday	08:30AM	10:30AM	A.0.6
Friday	09:30AM	11:30AM	A1.3

Room A1.3 is located at the first floor of the "Alan Turing" building.

Room A.0.6 is at the first floor of the "Renato Ricamo" building.

Free software for this course

• CMurphi
• SPIN
• NuSMV
• JUnit