The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Computer hardware and software can be modeled precisely in mathematical logic.
If expressed appropriately, these models can be executable. An
appropriate logic is an axiomatically formalized functional programming
language. This allows models to be used as simulation engines or rapid
prototypes. But because they are formal they can be manipulated by symbolic
means: theorems can be proved about them, directly, with mechanical theorem
provers. But how practical is this vision of machines reasoning about
machines? In this highly personal talk, I will describe the 40 year history of
Boyer-Moore Project and discuss progress toward making formal
verification practical. Among other examples I will describe important
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 have had
important functional properties verified. In addition, I will describe a model
of the Java Virtual Machine, including class loading and bytecode verification
and the proofs of theorems about JVM methods.
J Strother Moore holds the Admiral B.R. Inman Centennial Chair in Computing Theory at the University of Texas at Austin. He is the author of many books and papers on automated theorem proving and mechanical verification of computing systems. Along with Boyer he is a co-author 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 MIT in 1970 and his PhD from the University of Edinburgh in 1973. Moore was a founder of Computational Logic, Inc., and served as its chief scientist for ten years. He served as chair of the UT Austin CS department for eight years. He and Bob Boyer were awarded the McCarthy Prize in 1983 and the Current Prize in Automatic Theorem Proving by the American Mathematical Society in 1991. In 1999, they were awarded the Herbrand Award for their work in automatic theorem proving. Boyer, Moore, and Kaufmann were awarded the 2005 ACM Software Systems Award for the Boyer-Moore theorem prover. Moore is a Fellow of both the American Association for Artificial Intelligence and the ACM and is a member of the National Academy of Engineering.