Eric McCarthy

Eric McCarthy
Contact
e-mail: mccarthy@K.E, where K=kestrel and E=edu
address: see Contact page

Bio

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.