Presented by J Strother Moore, Department of Computer Sciences, University of Texas at Austin.

Abstract:
Computer hardware and software can be modelled precisely in mathematical logic. If expressed appropriately, these models can be executable. This allows them 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 45 year history of the “Boyer-Moore Project”, starting with its use to prove simple theorems by mathematical induction about list processing (e.g., the reverse of the reverse of x is x) to its routine use in the microprocessor industry (e.g., the floating point operations of the Via Nano 64-bit X86 microprocessor are compliant with the IEEE standard). Along the way we will see applications in program verification, models of instruction set architectures including the JVM, and security and information flow.

Biography:
J Strother Moore, professor emeritus at the University of Texas at Austin, held the Admiral B.R. Inman Centennial Chair in Computing Theory until his retirement in 2015.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. Boyer and Moore also invented the “piece table” data structure underlying Microsoft Word and a linear-time majority vote 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 from 2001-09 and led the $120M drive to build the Bill & Melinda Gates Center for Computer Science and Dell Computer Science Hall, opened in April, 2013.  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 Association for the Advancement of Artificial Intelligence, the ACM, the Royal Society of Edinburgh and the US National Academy of Engineering.