An Industrially Useful Prover
Duration: 60 mins
Share this media item:
Embed this media item:
Embed this media item:
About this item
| Description: |
Moore, J
Friday 7th July 2017 - 13:30 to 14:30 |
|---|
| Created: | 2017-07-24 17:35 |
|---|---|
| Collection: | Big proof |
| Publisher: | Isaac Newton Institute |
| Copyright: | Moore, J |
| Language: | eng (English) |
| Abstract: | 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. |
|---|---|
Available Formats
| Format | Quality | Bitrate | Size | |||
|---|---|---|---|---|---|---|
| MPEG-4 Video | 640x360 | 1.93 Mbits/sec | 869.23 MB | View | Download | |
| WebM | 640x360 | 558.64 kbits/sec | 245.50 MB | View | Download | |
| iPod Video | 480x270 | 495.91 kbits/sec | 217.93 MB | View | Download | |
| MP3 | 44100 Hz | 252.93 kbits/sec | 111.15 MB | Listen | Download | |
| Auto * | (Allows browser to choose a format it supports) | |||||