When I was a TA for my undergrad operating systems class, I gave a lecture once on using SPIN for basic verification of a handful of mutex implementations, and

When I was a TA for my undergrad operating systems class, I gave a lecture once on using SPIN for basic verification of a handful of mutex implementations, and proving a handful of properties about them. If you want a basic conceptual primer for Spin, I recommend checking it out -- here's a PDF of the slide deck: http://www.cs.cmu.edu/~410-s11/lectures/L38_SPIN.pdf http://www.cs.cmu.edu/~410-s11/lectures/L38_SPIN.pdf And here's a set of resources: http://www.cs.cmu.edu/~410-s09/lectures/L40_SPIN/spinfiles/ http://www.cs.cmu.edu/~410-s09/lectures/L40_SPIN/spinfiles/ Linked to from the above is another good resource from people who have used Spin -- a formal verification of Linux's RCU design, using Spin: http://lwn.net/Articles/243851/ http://lwn.net/Articles/243851/