2 ms·
A few links follow to show the power of the tool. Centaur, an x86 vendor, used it for formal verification of CPU's without paying huge money for typical tools:
by nickpsecurity 9y ago
A few links follow to show the power of the tool.
Centaur, an x86 vendor, used it for formal verification of CPU's without paying huge money for typical tools:
http://fm.csl.sri.com/LAW/2010/law2010-slides-Hunt.pdf http://fm.csl.sri.com/LAW/2010/law2010-slides-Hunt.pdf
Rockwell-Collins verifies a secure CPU, its microcode, and assembly on top of it:
http://www.ccs.neu.edu/home/pete/acl206/papers/hardin.pdf http://www.ccs.neu.edu/home/pete/acl206/papers/hardin.pdf
Original work on a verified stack that led to ACL2:
ftp://ftp.cs.utexas.edu/pub/boyer/fm9001/index.html