CDA 5416 Computer System Verification

The course description, requirements, and other information can be found in the syllabus..

Subjects/Slides	Reading
Introduction	Chapter 1
Intro. to SPIN	Basic Spin Manual Concise Promela Reference Check out Spin's website for more information about SPIN and Promela.
Background Review	Appendix
Modeling Concurrent Systems	Chapter 2, section 2.1, 2.2 (2.2.1 - 2.2.3, 2.2.6), 2.3
Linear-Time Properties	Section 3.1, 3.2.1 - 3.2.4, 3.3.1 - 3.3.2, 3.4.1, 3.5.1
Linear Time Logic	Section 5.1
Computation Tree Logic	Section 6.1 - 6.2, 6.3 (skim), 6.4, 6.5
Symbolic CTL Model Checking	Section 6.7.1 - 6.7.2
Binary Decision Diagrams	Section 6.7.3 - 6.7.4
Boolean Satisfiability Solving	Conflict-Driven Clause Learning SAT Solvers. More references at the end of slides
Bounded Model Checking	A paper on Bounded Model Checking by Armin Biere

Subjects/Slides

Reading

Chapter 1

Basic Spin Manual
Concise Promela Reference
Check out Spin's website for more information about SPIN and Promela.

Appendix

Chapter 2, section 2.1, 2.2 (2.2.1 - 2.2.3, 2.2.6), 2.3

Section 3.1, 3.2.1 - 3.2.4, 3.3.1 - 3.3.2, 3.4.1, 3.5.1

Section 5.1

Section 6.1 - 6.2, 6.3 (skim), 6.4, 6.5

Section 6.7.1 - 6.7.2

Section 6.7.3 - 6.7.4

References

A good book on using model checker SPIN, Principles of the Spin Model Checker, Mordechai Ben-Ari, Springer 2008, ISBN 978-1846287695.
(Available online for download if you are on the campus network.)
Information about model checker SPIN
Information about symbolic model checker nuXMV. It is derived from nuSMV, and their model languages share a lot of similarities. However, nuXMV has more diverse and more advanced algorithms supported in its background.
Information about symbolic model checker nuSMV including the tutorial on modeling in SMV language.