COMP4151 - Algorithmic Verification

Further Reading

• Logic in Computer Science, Michael Huth and Mark Ryan; 427 pages (2nd edition). Published by Cambridge University Press (link) in paperback only: ISBN 0 521 54310X, 2004
• The Spin Model Checker, G. Holzmann, 2003
• R.P. Kurshan Computer Aided Verification of Coordinating Processes (The automata theoretic approach) Princeton Series in CS, 1994
• Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, MIT Press 1994
  • E.A. Emerson, Temporal and Modal Logic,
  • W. Thomas, Automata on Infinite Objects

top

Tools

The NuSMV and SPIN model checker are installed on CSE linux machines. You can find them at:

• ~rhuuck/bin/NuSMV,
• ~rhuuck/bin/spin and GUI version at ~rhuuck/bin/xspin

It's best to set your PATH variable accordingly. I.e., if you're using bash as your shell of choice add:

PATH=.:~rhuuck/bin:whateverhasbeenherebefore:$PATH
export PATH

You can obtain all the documentation and install the tools themselves on your home machine if go to the web sites of NuSMV and SPIN.