Presented by:
J Strother Moore
Date:
Friday 7th July 2017 - 13:30 to 14:30
Venue:
INI Seminar Room 2
Event:
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.
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.
The video for this talk should appear here if JavaScript is enabled.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.
Presentation Material:
