BEGIN:VCALENDAR
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
SUMMARY:
Machines Reasoning about Machines
STATUS:CONFIRMED
ATTENDEE;CN="J Strother Moore
":
MAILTO:no@spam.com
DESCRIPTION:
Computer hardware and software can be modeled precisely in m
athematical logic. If expressed appropriately\, these models
can be executable. An appropriate logic is an axiomatically
formalized functional programming language. This allows mod
els to be used as simulation engines or rapid prototypes. Bu
t because they are formal they can be manipulated by symboli
c means: theorems can be proved about them\, directly\, with
mechanical theorem provers. But how practical is this visio
n of machines reasoning about machines? In this highly perso
nal talk\, I will describe the 40 year history of the Boyer-
Moore Project and discuss progress toward making formal veri
fication practical. Among other examples I will describe imp
ortant theorems about commercial microprocessor designs\, in
cluding parts of processors by AMD\, Motorola\, IBM\, Rockwe
ll-Collins and others. Some of these microprocessor models e
xecute at 90% the speed of C models and have had important f
unctional properties verified. In addition\, I will describe
a model of the Java Virtual Machine\, including class loadi
ng and bytecode verification and the proofs of theorems abou
t JVM methods. Biography J Strother Moore holds the Admiral
B.R. Inman Centennial Chair in Computing Theory at the Unive
rsity of Texas at Austin. He is the author of many books and
papers on automated theorem proving and mechanical verifica
tion of computing systems. Along with Boyer he is a co-autho
r of the Boyer-Moore theorem prover and the Boyer-Moore fast
string searching algorithm. With Matt Kaufmann he is the co
-author of the ACL2 theorem prover. Moore got his SB from MI
T in 1970 and his PhD from the University of Edinburgh in 19
73. Moore was a founder of Computational Logic\, Inc.\, and
served as its chief scientist for ten years. He served as ch
air of the UT Austin CS department for eight years. He and B
ob Boyer were awarded the McCarthy Prize in 1983 and the Cur
rent Prize in Automatic Theorem Proving by the American Math
ematical Society in 1991. In 1999\, they were awarded the He
rbrand Award for their work in automatic theorem proving. Bo
yer\, Moore\, and Kaufmann were awarded the 2005 ACM Softwar
e Systems Award for the Boyer-Moore theorem prover. Moore is
a Fellow of both the American Association for Artificial In
telligence and the ACM and is a member of the National Acade
my of Engineering.
DTSTART;TZID=Europe/Paris:20101026T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201010261
100
UID:LSVsemLSV.201010261100@lsv.ens-cachan.fr
LOCATION:Salle de ConfĂ©rence (Pavillon des Jardins)
END:VEVENT
END:VCALENDAR