01
ACL2 and the Industrialization of Automated Theorem Proving
ACL2 turned the Boyer-Moore tradition of automated inductive theorem proving into an executable Common Lisp-based logic that could model and verify commercial hardware and software systems.
↗