[Colloq] Visitor Talk: Jared Davis "The Milawa theorem prover is sound down to the x86 machine code that runs it" Friday July 13th at 11:00am

[Nicole Bekerian]

The College of Computer and Information Science presents:

Speaker: Jared Davis, Centaur Technology
         Joint work with Magnus Myreen (Cambridge)

Title: The Milawa theorem prover is sound down to the x86 machine code that runs it
Location: 366 WVH
Date & Time: 11:00am on Friday July 13th

Host: Pete Manolios

Abstract:

Boyer-Moore theorem provers, like NQTHM and ACL2, are very "pragmatic."  They have complex proof procedures that aren't verified and don't produce any justification of their claims.

Milawa is a new, simplified Boyer-Moore style prover with a completely opposite, "pure" design.

We start with a small, simple, logical kernel.  This kernel has a reflection mechanism that allows it to reason about new proof procedures.  After a new proof procedure has been shown to be sound, the kernel can freely use it in subsequent proofs, and the algorithm does not need to justify its work.

Using this mechanism, we guide the kernel to verify that all of Milawa's proof procedures (rewriting, etc.) are sound.  This process "grows" the kernel into a useful theorem prover.  It also reduces the question of trusting Milawa's proof procedures to that of trusting its kernel.

Then we go further. We have designed a new Lisp runtime that can run the kernel.  Using the HOL4 theorem prover (itself a rather pure system), we have verified this runtime down to the concrete x86-64 machine code.  Along with
HOL4 proofs that show the Milawa logic is sound and that the source code for the Milawa kernel obeys the logic, we arrive at our top-level theorem: no matter how reflection or any other operation is used, Milawa can never prove a formula that isn't true.

Bio:

Jared Davis received his PhD at the University of Texas at Austin in 2009, where he developed Milawa, "a self-verifying theorem prover."  Since that time he has worked in formal hardware verification at Centaur Technology in Austin, TX, a company that designs x86 processors for its parent company, VIA.


-- 




Best, 
Nicole 

______________________________________________________________ 

Nicole Bekerian 
Administrative Assistant 

Northeastern University 
College of Computer and Information Science 
360 Huntington Ave. 
202 West Village H 
Boston, MA 02115 

Phone: 617.373.2462 
Fax: 617.373.5121