Hyperkernel – A push-button approach to building provably correct OS kernels

Re:Hyperkernel – A push-button approach to building provably... by snaky on Wednesday September 12, 2018 @08:35AM (#17967898)

> ACL2 has had numerous industrial applications. In 1995, J Strother Moore, Matt Kaufmann and Tom Lynch used ACL2 to prove the correctness of the floating point division operation of the AMD K5 microprocessor in the wake of the Pentium FDIV bug. The interesting applications page of the ACL2 documentation has a summary of some uses of the system. Industrial users of ACL2 include AMD, Centaur Technology, IBM, Intel, Oracle, and Rockwell Collins. ACL2 is intended to be an "industrial strength" version of the Boyer–Moore theorem prover, NQTHM.

https://en.wikipedia.org/wiki/ACL2

NQTHM was used to check e.g. FM9001 CPU

ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/nqthm-bibliography.html

B. Brock, W. A. Hunt, and M. Kaufmann. The FM9001 Microprocessor Proof. Tech. Rept. 86, Computational Logic, Inc., 1994. ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/086.pdf

[ Parent | on HN ]

Re:Hyperkernel – A push-button approach to building provably... by tonyg on Wednesday September 12, 2018 @10:13AM (#17968962)

J Strother Moore has some good slides on industrial applications of ACL2 here: https://www.inf.ed.ac.uk/teaching/courses/ar/j_moore_sprint-...

[ Parent | on HN ]