11410 Windermere Meadows
Austin, TX 78759-4551 USA
1 (512) 758-9967
I'm originally from Omaha, Nebraska. I studied computer science at UT Austin and completed my Ph.D. in 2009. I then worked for many years at a wonderful little company, Centaur Technology, developing tools and working to analyze X86 processor designs, mostly using the ACL2 theorem prover. On the side I started Kookamara LLC for freelance consulting.
It's an exciting time for me—after 8 great years at Centaur and a good run with Kookamara, I've just started a new full-time job with the great formal verification group at Apple.
My dissertation project, Milawa, was a self-verifying theorem prover. It starts with a small proof checker that can be extended with new proof techniques. These extensions can be verified by the proof checker so that they do not reduce our trust in the system. Through a series of many extensions, the proof checker grows into an ACL2-like theorem prover.
Going beyond the prover itself, Magnus Myreen developed Jitawa, a verified Lisp runtime that is capable of hosting Milawa and running through its entire bootstrapping process. Magnus went on to prove, using HOL4, that Milawa is sound all the way down to x86 machine code when run on this Lisp!
Our final, comprehensive Milawa/Jitawa paper is now available in the Journal of Automated Reasoning:
The reflective Milawa theorem prover is sound (down to the machine code that runs it). Jared Davis and Magnus O. Myreen. Journal of Automated Reasoning. Springer. August, 2015. Volume 55(2), Pages 117-183.
Check it out!
Some select publications:
Full list of publications, with abstracts.
I've worked a lot with the ACL2 Theorem Prover, most of which is described in various sections of the ACL2+Books Manual. A few highlights:
Most ACL2 development happens at Github, see the Community Books project.
Long ago I wrote Aiksaurus, an English-language thesaurus. I haven't worked on it in many years, but it appears to still be alive and well.
Most Linux users can also just: