VSTTE2012 verification competition で使われてたツールをメモ:
Coq http://coq.inria.fr/
Dafny http://research.microsoft.com/dafny
Ssreflect http://www.msr-inria.inria.fr/Projects/math-components
VCC http://vcc.codeplex.com
ATS http://www.ats-lang.org/
Perfect Developer http://www.eschertech.com/products/perfect_developer.php
Escher C Verifier http://www.eschertech.com/products/ecv.php
Isabelle/HOL http://isabelle.in.tum.de/
HolFoot http://holfoot.heap-of-problems.org/
B Method with Atelier B tool http://www.atelierb.eu/en/
PVS http://pvs.csl.sri.com/
Socos http://www.imped.fi/socos/