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. I'm now part of the formal verification group at Apple.
My dissertation project, Milawa, was a self-verifying theorem prover. It starts as a small proof checker that can be extended with new proof techniques. The proof checker can verify these extensions so that they don't reduce our trust in the system. Through a bootstrapping process, the proof checker is extended many times and 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 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: