Download fulltext - DiVA Portal

8.3 Where to go from here
8.3.5
8 CONCLUSION
Evaluation of alternatives for formal verification
A lot of research is done in the field of formal verification of software today and
there exists a number of tools and documents about it. In places where formal
verification can be done testing simply can’t compete, formal verification
can show that a requirement holds for all cases where testing only can show
correctness for a tiny fraction of all possible cases.
Technologies of interest:
• Cryptol - http://www.cryptol.net
• Isabelle - http://www.cl.cam.ac.uk/research/hvg/Isabelle
• ACL2 - http://www.cs.utexas.edu/ moore/acl2
• Coq - http://coq.inria.fr
27