- By Phone...
- Mobile: 1 (512) 758-9967
- Work: 1 (512) 418-5736
- Skype: jared.c.davis (often idle)
- By IRC...
- irc.freenode.net#ccl (clop)
- By Email...
- By Tortise...
- Jared Davis
- 11410 Windermere Meadows
- Austin, TX 78759-4551 USA
- Magnus O. Myreen and Jared Davis. The reflective Milawa theorem prover is sound (down to the machine code that runs it) . In ITP 2014. Pages 421-436.
- Jared Davis, Anna Slobodova, and Sol Swords. Microcode Verification—Another Piece of the Microprocessor Verification Puzzle. Invited talk, ITP 2014. Pages 1-16.
- Jared Davis and Matt Kaufmann. Industrial Strength Documentation for ACL2. In ACL2 2014. July, 2014. EPTCS 152. Pages 9-25.
Other Selected Publications
- Jared Davis and Sol Swords. Verified AIG Algorithms in ACL2. In ACL2 2013. May, 2013. EPTCS 114. Pages 95-110.
- Jared Davis. Embedding ACL2 Models in End-User Applications. In Do-Form 2013. April, 2013, Exeter, UK.
Full list of publications, with abstracts.
Most of my work has to do with the ACL2 theorem prover. You may be interested in:
- Kookamara -- ACL2 development for hire.
- The ACL2 Books project
- The ACL2 XDOC Manual
- Older ACL2 Projects
- My dissertation project, Milawa, is a small proof checker which can be extended with new proof techniques. Extensions can be verified by the small, trusted core so that new capabilities do not reduce our trust in the system.
Old Projects — I don't work on these anymore.