http://www.cs.utexas.edu/~marijn/publications/ACL2-ARCADE.pdf http://www.cs.utexas.edu/~marijn/publications/ACL2-ARCADE.pd... Uses in industry: • verification

http://www.cs.utexas.edu/~marijn/publications/ACL2-ARCADE.pdf http://www.cs.utexas.edu/~marijn/publications/ACL2-ARCADE.pd... Uses in industry: • verification of all elementary floating-point arithmetic on the AMD Athlon, after running 100M test vectors successfully comparing the ACL2 model with the AMD RTL simulator; • verification of all elementary floating-point arithmetic on the AMD Opteron; • verification of a silicon implementation of a JVM chip by Rockwell-Collins; • verification of the Rockwell Collins AAMP7 crypto chip (the basis for obtaining NSA MILS certification); • verification of the Greenhills operating system; • verification of important invariants in the Sun JVM class loader and properties assured by the Sun byte-code verifier; • verification of the Centaur Technology, Inc., Verilog design for the VIA Nano floating point adder which handles 32-bit, 64-bit, and 80-bit additions, is pipelined to deliver 4 results per cycle, has 1074 input signals including 26 clock signals and 374 output signals, consists of 33,700 lines of Verilog in 680 modules requiring 432,322 transistors; • checking of a computationally surveyable proof of important properties of an Intel implementation of the elliptic curve key agreement including that 2^255 − 19 is prime and that the elliptic curve known as Curve25519 is an abelian group; • verification of floating point designs at Oracle and ARM.