Seminár z teoretickej informatiky - Warren A. Hunt (31.5.2018)

mimoriadne vo štvrtok 31.5.2018 o 11:00 hod. v posluchárni M/213

28. 05. 2018 18.01 hod.
Od: Rastislav Královič

Prednášajúci: Warren A. Hunt, Jr.

Názov: Industrial Hardware and Software Verification with ACL2

Termín: 31.5.2018, 11:00 hod., M/213

Abstrakt:
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.

Spoluautori: Matt Kaufmann, J Strother Moore (Dept. of Computer Science, UT Austin) Anna Slobodova (Centaur Technology, Inc. Austin, Texas)

web: http://kedrigern.dcs.fmph.uniba.sk/STI2
rss: http://kedrigern.dcs.fmph.uniba.sk/STI2/rss.php