Patrick Trentin

Laboratory of Formal Methods (2017/2018)

The material is made available after each lesson.

Disclaimer: last year's slides will be subject to some changes, thus refer to the updated content.

All packages can be opened with the command
~$ tar -xvf package_name.tar.gz

Part I - spin

The spin model checker can be downloaded from this link.
Its documentation is provided here.

• Spin: Introduction - February 23, 2018
  Spin: Introduction (slides)
  Lab examples (download)


• Spin: Overview of PROMELA - March 02, 2018
  Spin: Overview of PROMELA (slides)
  Code examples (download)
  Exercises solutions (download)


• Spin: Exercises on Message Channels - March 09, 2018
  Spin: Exercises on Message Channels (slides)
  Code examples (download)
  Exercises solutions (download)


• Spin: LTL Model Checking - March 16, 2018
  SPIN: LTL Model Checking (slides)
  Code examples (download)
  Exercises solutions (download)
  Optional Exercise solution (download)


• Spin: Exercises - Part A - April 11, 2018 (10.30 - 12.30)
  Spin: Exercises - Part A (slides)
  Exercises solutions (download)


• Spin: Exercises - Part B - April 18, 2018 (10.30 - 12.30)
  Spin: Exercises - Part B (slides)
  Exercises solutions (download)

Part II - nuXmv

The nuXmv model checker can be downloaded from this link.
Its documentation is provided here.

• nuXmv: Introduction - April 27, 2018
  nuXmv: Introduction (slides)
  Code examples (download)
  Exercises solutions (download)
  


• nuXmv: Model Checking - May 04, 2018
  nuXmv: Model Checking (slides)
  Code examples (download)
  Exercises solutions (download)
  


• nuXmv: Planning - May 09, 2018 (14.30 - 16.30)
  nuXmv: Planning (slides)
  Code examples (download)
  Exercises solutions (download)
  


• nuXmv: Bounded Model Checking - May 18, 2018
  nuXmv: Bounded Model Checking (slides)
  Code examples (download)
  Exercises solutions (download)
  Optional Exercise solution (download)
  


• nuXmv: Exercises - Part A - May 25, 2018
  nuXmv: Exercises - Part A (slides)
  Exercises solutions (download)
  Optional Exercise solution (download)
  


• nuXmv: Exercises - Part B - June 01, 2018
  nuXmv: Exercises - Part B (slides)
  Code examples (download)
  Exercises solutions (download)
  

Lecture Schedule:
Every Friday,
9.30-11.30 AM
PC Room A201

Office Hours:
On appointment,
(send an email)

Course Evaluation:
Written exam

Past Exams:
download (updated: 06/09/2018)

Docs for Exam:
download (found in '/usr/local/docs')