University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > An Industrially Useful Prover

An Industrially Useful Prover

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact info@newton.ac.uk.

BPR - Big proof

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.



This talk is part of the Isaac Newton Institute Seminar Series series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity