2110 N 89th St
Seattle WA 98103
Overview The person other software engineers come to when they think they're stuck
Work Coverity, August 2009 to present, acquired by Synopsys in 2014
Software developer, tech lead, and manager for static and dynamic program analysis projects.
  • New code checkers (two patents pending): Coverity software automatically finds coding mistakes that matter to programmers, by going much deeper and by being more clever and more cautious than linters. I conceived, designed, implemented, and/or oversaw many successful checkers for new bug patterns. My solo patent relates to finding mistyped identifiers in dynamic languages.
  • New language support: I have been a key contributor, tech lead, or project owner for almost every extension of Coverity's famous C/C++ analysis engine to another programming language, including support for Java, C#, JavaScript, PHP, Python, and Ruby. For the last three, I architected, negotiated, and delivered on a strategy for rapid support of new languages, the winning strategy because it avoided technical debt and brand deterioration.
  • Web application security: I designed and implemented several key components of our first release of Java web application security analysis, mostly relating to finding XSS (cross-site scripting) defects with high accuracy and sensitivity. Four years later, my components have endured with little maintenance or even enhancement.
Most development in C++, some in Java, plus a bit in C#, Perl, Python, etc.
Promotions: Senior Engineer, 2010. Principle Engineer, 2013. Manager, 2015.
Education Doctor of Philosophy in Computer Science · Northeastern University, 2007 - 2010; transfer with advisor from Georgia Tech, 2003 - 2007
  • Adaptive Approximate State Storage (thesis research):  Explicit-state model checkers use approximate (probabilistic) state storage techniques such as Bloom filters to reduce memory requirements by orders of magnitude while maintaining very high defect detection ability. I made key improvements to Bloom filters (find my name on the Wikipedia page) to make them simultaneously fast and accurate. This work was integrated into the award-winning model checker Spin.

    I then developed a much more advanced system for approximate state storage that simultaneously (a) has strong information-theoretic properties, (b) outperforms alternatives in many cases, and (c) adapts on-the-fly to an arbitrary state space size, making it more user-friendly.

  • ACL2s: "The ACL2 Sedan" (assistantship research, 2005 - 2009):  I am the initial developer of ACL2s, an Eclipse-based development environment for the award-winning ACL2 theorem proving system.

Master of Science in Computer Science · Georgia Tech · 2002 - 2003
Bachelor of Science in Computer Science · Georgia Tech · 1999 - 2002
  • Highest honors designation on Bachelor's (3.70 / 4.00 GPA)
  • Areas of focus: Compilers, Languages, Program Analysis, Testing, Formal Methods, Operating Systems, Artificial Intelligence, Theory, Algorithms
Publications (peer-reviewed)
  • Fast, All-Purpose State Storage. SPIN Workshop, 2009.
    Coauthor: Panagiotis Manolios.
  • Hacking and Extending ACL2. ACL2 Workshop, 2007.
    Coauthors: Matt Kaufmann and Panagiotis Manolios.
  • ACL2s: "The ACL2 Sedan". Workshop on User Interfaces for Theorem Proving (UITP), 2006.
    Coauthors: Panagiotis Manolios, J Moore, and Daron Vroon. (Another version was a demo at ICSE 2007.)
  • Bloom Filters in Probabilistic Verification. Conference on Formal Methods in Computer-Aided Design (FMCAD), 2004.
    Coauthor: Panagiotis Manolios.
  • Fast and Accurate Bitstate Verification for SPIN. SPIN Workshop, 2004.
    Coauthor: Panagiotis Manolios.
Internships Research Intern · NASA Ames Research Center · Summer 2006
Robust Software Engineering group, under Willem Visser, Corina Pasareanu, and Peter Mehlitz
  • State Matching in Java PathFinder:  JPF is an explicit-state model checker for concurrent Java programs. I retooled the state hashing and matching system to be much faster and provide highly configurable and customizable state abstractions.
Research Intern · NASA/Caltech Jet Propulsion Laboratory · Summer 2004
Laboratory for Reliable Software, under Gerard Holzmann and Rajeev Joshi
  • Integrated some of my data structure enhancements into an official release of the Spin model checker (in addition to other small projects)
Teaching Instructor of Record · Northeastern University · Fall 2008
CS U290: "Logic and Computation," a relatively new class introducing freshman students to logic through the ACL2 programming language, logic and theorem prover. Students use my ACL2s development environment.
  • Developed all lectures, assignments, and tests, loosely based on previous term.
Instructor · Georgia Governor's Honors Program · Summers 2005 & 2007
Math department, under Dennis Stewart and Dale Lyles
  • Developed my own curricula for summer enrichment courses for enthusiastic high school students
  • Taught courses on Cryptography, Logic, Theory of Computation, Functional Programming, and Introductory Programming.
Teaching assistant · Georgia Tech and Northeastern University · 2000 - 2003, 2008
References Available upon request
Community Vice president, board member, and section leader in San Francisco Lyric Chorus, 2009 - 2013
U.S. Citizen