SPIN
Freely available model checker
Developed at Bell Labs by Gerard Holzmann for modeling hardware communication protocols
Verifies programs written in Promela
Receptive to bug fixes and suggestions
Previous
Next
Index
Picture