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

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

An Industrially Useful Prover

Download to your calendar using vCal

If you have a question about this talk, please contact INI IT .

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.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Vital Geographies - Department of Geography Mathematics and Machine Learning Hybrid: in-person in Cambridge & online via Teams

Other talks

Group Presentation 5 Title to be confirmed Laser tomography for wide area gas emission spatio-temporal reconstruction Title and abstract tba Title to be confirmed FILM: One With The Whale
 

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