I'm Jared Davis — Kookamara is my company for freelance consulting.
I specialize in formal hardware and software verification, usually with ACL2.
I would be excited to help with your verification efforts.
I have 11 years of ACL2 experience including
- Full-time industrial ACL2 work at Centaur Technology and Rockwell Collins
- Ph.D. research at UT Austin, the home of ACL2, verifying an ACL2-like prover
I am a primary author of ACL2 libraries including
- Core libraries like cutil, std, str, osets, unicode and xdoc
- Centaur libraries like vl, esim, bitops, bridge, aig, ubdd, and 4v
- Coi libraries like adviser, alists, dtrees, lists, and maps
I am a primary author of the ACL2(h) extension including
- The serialization routines for working with galactic objects
- The implementation of hons and fast association lists
I am a leader in the ACL2 community
- Founder and administrator of the ACL2 Community Books project
- Member of the gold-medal ACL2 team in the VSTTE 2012 competition
- Editor of the ACL2 Workshop 2013
- Author of many ACL2-related academic papers
I have broad experience beyond ACL2, including
- Hardware description languages (Verilog)
- Systems programming languages (C, C++, Java, assembly)
- Scripting languages (Ruby, Perl, etc), build systems, and Unix in general
- Lisp, ML, and other functional languages
- Multithreading, networking, IPC, GUIs, GPGPU, databases, parsers, ...
Let's Get Started
If this sounds like a good fit for your projects, let's chat.
- 11410 Windermere Meadows
- Austin, TX 78759