mccarthy@K.E, where K=kestrel and E=edu
My primary interest is formal verification of R1CS (Rank 1 Constraint Systems), which are used for zero knowledge proofs such as zk-SNARKs and bulletproofs.
I am also working on the ACL2 Ethereum project.
My past work includes:
- The DerivationMiner project, where I developed (in Python) the “big code” pipeline we used to process and run machine learning on a corpus of 23 TB. I saved Java bytecode and artifacts to a Titan graph database, and ran NMF for dimension reduction. I also developed our code similarity search tool. I would like to apply these “big code” tools to corpora of smart contract code. I also learned how to use the ACL2 theorem prover and did some formal verification as part of this project.
- The VIBRANCE project, where we automatically hardened Java bytecode against attacks from tainted inputs.
- With Decidable Software, developed a tool using Software Refinery to automate a large source code port from a proprietary PL/I-like language to standard COBOL for a French customer. Recruited two additional full-time developers for this project.
- Architect and lead developer for tools used in reinspection service, written in Python and Java. (Reasoning, post-Y2K era)
- Implemented a distributed processing system for large analysis jobs. (Reasoning, Y2K era)
- UX/UI design and implementation for Y2K analysts. (Reasoning, Y2K era)
- Extended Intervista UI toolkit and Dialect grammar compiler to handle Japanese text. (Reasoning, Software Refinery era)
- Software Refinery core developer for 15 years, bringing into production the Refine IDE, Dialect grammar compiler, Intervista UI toolkit, REFINE/Ada, REFINE/C, REFINE/COBOL, and REFINE/FORTRAN static analysis products. Programming in Lisp and Refine.
I received a degree in Mathematical Sciences from Stanford University in 1984.