skip to content

An Industrially Useful Prover

Presented by: 
J Strother Moore University of Texas at Austin, University of Edinburgh
Friday 7th July 2017 - 13:30 to 14:30
INI Seminar Room 2
The ACL2 theorem prover is an interactive  automatic prover for the programming language
Common  Lisp.  It provides a convenient language for
building  prototypes of hardware and
software designs,  algorithms, and other
computing systems.  In fact, the  language is executed efficiently enough to
permit some  practical systems to be
built in it.  But ACL2 also  provides an environment for proving theorems
about  those prototypes.  In this talk I will demonstrate how

 ACL2 presents
itself to the user, show a small example 
proof project about low-level code, and discuss the  aspects of ACL2 that have made it attractive
as a tool  for industry.
Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons