« Formal Methods in Use at Galois | Main | Beautiful Parallelism: Harnessing Multicores with Haskell »

Tech Talk: Mechanically verified LISP interpreters

This week's tech talk will be Magnus Myreen from Cambridge talking about mechanically verified Lisp interpreters. It will be held at the irregular time of 2pm, Friday Nov 14.
This talk describes work on constructing verified interpreters for a small LISP-like language using the interactive theorem prover HOL4.  The LISP interpreters have been proved correct with respect to detailed x86, ARM and PowerPC processor models (written by Sarkar, Fox and Leroy). New techniques for expressing correctness of machine code were developed, as well as new techniques for proof-producing decompilation and compilation to/from HOL4 functions. A copying garbage collector (a Cheney collector) was verified and subsequent proofs were built upon its verified specification.

Reader Comments (1)

Do you record tech talks you host?

November 15, 2008 | Unregistered CommenterVyacheslav Egorov

PostPost a New Comment

Enter your information below to add a new comment.

My response is on my own website »
Author Email (optional):
Author URL (optional):
Some HTML allowed: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <code> <em> <i> <strike> <strong>