Laboratory of Formal Methods (2015/2016)
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 -
Feb 26, 2016
Spin: Introduction (slides)
Lab examples (download)
-
Spin: Overview of PROMELA -
Mar 04, 2016
Spin: Overview of PROMELA (slides)
Code examples (download)
Exercises solutions (download)
-
Spin: Exercises on Message Channels -
Mar 11, 2016
Spin: Exercises on Message Channels (slides)
Code examples (download)
Exercises solutions (download)
-
Spin: LTL Model Checking -
Mar 18, 2016
SPIN: LTL Model Checking (slides)
Code examples (download)
Exercises solutions (download)
Optional Exercise solution (download)
-
Spin: Exercises - Part A -
Apr 01, 2016
Spin: Exercises - Part A (slides)
Exercises solutions (download)
-
Spin: Exercises - Part B -
Apr 08, 2016
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 -
Apr 15, 2016
nuXmv: Introduction (slides)
Code examples (download)
Exercises solutions (download)
-
nuXmv: Model Checking -
Apr 22, 2016
nuXmv: Model Checking (slides)
Code examples (download)
Exercises solutions (download)
-
nuXmv: Planning -
Apr 29, 2016
nuXmv: Planning (slides)
Code examples (download)
Exercises solutions (download)
-
nuXmv: Bounded Model Checking -
May 06, 2016
nuXmv: Bounded Model Checking (slides)
Code examples (download)
Exercises solutions (download)
Optional Exercise solution (download)
-
nuXmv: Exercises - Part A -
May 13, 2016
Code examples (download)
nuXmv: Exercises - Part A (slides)
Exercises solutions (download)
-
nuXmv: Exercises - Part B -
May 20, 2016
nuXmv: Exercises - Part B (slides)
Exercises solutions (download)
Part III - Wrapping Up
-
Exam: Simulation -
May 27, 2016
Exam: Simulation (solution & results)
Available documentation during the exam (download) - found in '/usr/local/docs'
Past exams and solutions (download)
-- last update: 02/09/2016