A SPIN modellellenőrző rendszer egy széles körben alkalmazott program osztott
szoftver rendszerek időzítéstől független tulajdonságainak formális, automatikus
ellenőrzésére. 2002 áprilisában e program nyerte el az ACM (Association for
Computing Machinery), évenként odaítélt, igen rangos Szoftver Rendszer Díját (A
Software System Award-ot). Ezzel a kitűntetéssel, korábban olyan rendszereket
jutalmaztak, mint a Unix, TeX, TCP/IP, Tcl/Tk és a Java.
A kurzus a logikai modellellenőrzés gyakorlatába kíván bevezetést nyújtani a SPIN rendszer használata segítségével. Célja konkrét példákon keresztül bemutatni, hogyan lehet egyidejű(konkurens), többszálú rendszereket a SPIN segítségével modellezni, rájuk formális specifikációkat megfogalmazni és azokat ellenőrizni.