[Pl-seminar] Fwd: 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

[Aaron Turon]

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.