Overview of FM Tools

• Theorem Provers (e.g. PVS)
  • requires axioms and preconditions
  • requires skilled intervention
• Model Checkers (e.g. SPIN)
  • state space explosion
  • accessible tools