Model checking using Spin
Spin version 6.4.6
.
Introduction to model-checking using Spin
Spin models used in class:
Mod-4 counter
.
Traffic light
.
Traffic light, fixed version
.
LTL model-checking
.
Some
Lecture Notes
on B\"uchi automata and LTL model-checking.
Book
Chapter
by Madhavan Mukund on Finite-state Automata on Infinite Inputs, in Modern Applications of Automata Theory (World Scientific/IISc Press).
Assignment 2
due on Mon 17th Feb 2020.