PRL Seminars

ACL2 is an industrial-strength version of the Boyer-Moore theorem prover. It has been used to establish the correctness of the RTL for all the elementary floating point arithmetic on AMD's Athlon microprocessor, to analyze a security model for the IBM 4758 cryptoprocessor, to establish equivalence between two microarchitectures at Rockwell Collins Avionics, and to model the Java Virtual Machine. In this talk, I will simply demonstrate ACL2 live on simple examples and we can explore issues as they come up.