ACL2 is designed to support automated reasoning in inductive logical theories, mostly for the purpose of software and hardware verification.
ACL2 |
He and others used ACL2 to prove the correctness of the floating point division operations of the AMD K5 microprocessor in the wake of the Pentium FDIV bug.