SPIN:
• SPIN generates C program that is the model checker
– The pan verifier
• Process Analyzer
– Run the pan executable to do the model checking
• SPIN simulation modes
– Random: SPIN randomly makes decisions
– Interactive: User interactively makes decisions
– Guided: Analyze failed verification
• Trail files