BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Machines Reasoning about Machines  
DTSTART:20110607T101500
DTSTAMP:20260407T185130Z
UID:d5c3a54a7fadabd80424ab55e81dd85a96c30595723761cc38536d71
CATEGORIES:Conferences - Seminars
DESCRIPTION:Prof. J Strother Moore\, University of Texas at Austin\, Keyno
 te Speaker\nComputer hardware and software can be modeled precisely in mat
 hematical logic. If expressed appropriately\, these models can be executab
 le. An ``appropriate'' logic is an axiomatically formalized functional pro
 gramming language. This allows models to be used as simulation engines or 
 rapid prototypes. But because they are formal they can be manipulated by s
 ymbolic means: theorems can be proved about them\, directly\, with mechani
 cal theorem provers. But how practical is this vision of machines reasonin
 g about machines? In this highly personal talk\, I will describe the 40 ye
 ar history of the ``Boyer-Moore Project'' and discuss progress toward maki
 ng formal verification practical. Among other examples I will describe imp
 ortant theorems about commercial microprocessor designs\, including parts 
 of processors by AMD\, Motorola\, IBM\, Rockwell-Collins and others. Some 
 of these microprocessor models execute at 90% the speed of C models and ha
 ve had important functional properties verified. In addition\, I will desc
 ribe a model of the Java Virtual Machine\, including class loading and byt
 ecode verification and the proofs of theorems about JVM methods. Prof. J S
 trother Moore's homepage
LOCATION:CO-1
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR