Model Checking

• Bogor
• Cadena
• ESC/Java2
• Java Path Finder (JPF) a system to verify executable Java bytecode programs.
• JML The Java Modeling Language
• MLAT Modal Logic Abstraction Tool
• PRISM Probabilistic Symbolic Model Checker
• SLAM
• SMV Symbolic Model Verifier
• SPIN On the Fly, LTL Model Checker
• TVLA 2 3-Valued Logic Analysis Engine