Jens Bendisposto:Model Checkers

• SPIN http://spinroot.com/spin/whatispin.html
• PAT http://www.comp.nus.edu.sg/~pat/
• MALPAS http://www.atkinsglobal.co.uk/sectors-and-services/sectors/defence/documents/~/media/Files/A/Atkins-UK/Attachments/sectors/defence/library-docs/capability-statements/malpas.pdf
• Mocha http://www.cis.upenn.edu/~mocha/
• Prism http://www.prismmodelchecker.org/
• NuSMV http://nusmv.fbk.eu/
• PVS http://pvs.csl.sri.com/
• COMPASS http://compass.informatik.rwth-aachen.de/about.html
• COSPAN
• SMV Symbolic Model Verifier http://www.cs.cmu.edu/~modelcheck/smv.html http://www.kenmcmil.com/smv.html
• NuSMV http://nusmv.fbk.eu/
• Murphi http://www.cs.utah.edu/formal_verification/Murphi/
• XMC
• BLAST http://mtc.epfl.ch/software-tools/blast/index-epfl.php
• DiVinE http://divine.fi.muni.cz/
• Solibri http://www.solibri.com/
• Bogor http://bandera.projects.cis.ksu.edu/ http://bogor.projects.cis.ksu.edu/
• MCK http://cgi.cse.unsw.edu.au/~mck/pmck/
• YASM http://www.cs.toronto.edu/~arie/yasm/
• SLAM http://research.microsoft.com/en-us/projects/slam/