RiSE Invited Lecture: Warren Hunt

Date: 17:00, Wednesday, May 30, 2018
Speaker: Warren Hunt
Venue: TU Wien, Seminarraum 127 (Gußhausstr. 25-29 - Stiege 1 - 3.Stock)

Abstract:
The ACL2 theorem-proving system has seen sustained industrial use since
the mid 1990s.  Companies that have and are using ACL2 include AMD, ARM,
Centaur Technology, General Electric, IBM, Intel, Kestrel Institute,
Motorola/Freescale, Oracle, and Rockwell Collins.  ACL2 has been
accepted for industrial application because it is an integrated
programming/proof environment supporting a subset of the ANSI standard
Common Lisp programming language.  Software and hardware systems have
been modeled and analyzed with the ACL2 theorem-proving system.

The ACL2 programming language can be used to develop efficient and
robust programs.  The ACL2 analysis machinery provides many features
permitting domain-specific, human-supplied guidance at various levels
of abstraction.  ACL2 specifications often serve as efficient execution
engines for the modeled artifacts while permitting formal analysis and
proof of properties.  ACL2 provides support for the development and
verification of other formal analysis tools.  ACL2 did not find its way
into industrial use merely because of its technical features.  The ACL2
user/development community has a shared vision of making formal
specification and mechanized verification routine — we have been
committed to this vision for the quarter century since the Computational
Logic, Inc., Verified Stack.

Posted in RiSE Seminar