I am a Computer Scientist in the Center for Applied Scientific Computing (CASC) at Lawrence Livermore National Laboratory (LLNL). My research interests are in the fields of programming languages and applied formal methods. My recent work is on binary analysis, building certified systems in the Coq proof assistant, and making Coq proofs easier. I am broadly interested in the application of PL/FM to systems, networking, and security; and on easing the burden of certified programming.

My personal email address is and my LLNL contact info is here.

Before this, I had the pleasure of working with Julien Vanegue and the CTO security group at Bloomberg LP, doing a postdoc with Greg Morrisett at Cornell, and earning a PhD at UCSD with Nadia Polikarpova and Sorin Lerner in the Programming Systems group.

Here are some of my current and past projects!

  • LambDelphi: learned models for estimating the difficulty of proofs.
  • mirrorsolve: extensible first-order logic in Coq with an SMT solver backend. talk with demo, code.
  • leapfrog: certified, automatic proofs of equivalence for network protocol parsers. blog post, code.
  • mockdown: resizeable visual layouts from input-output examples. replication package, code.
  • spyder: language support for maintaining data invariants. code.
  • eddie: interactive diagrams without coding. website, code.


Conference Publications

Leapfrog: Certified Equivalence for Protocol Parsers

Ryan Doenges, Tobias Kappé, John Sarracino, Nate Foster, Greg Morrisett. PLDI '22. talk, pdf.

Synthesis of Web Layouts from Examples

John Sarracino1, Dylan Lukes1, Cora Coleman, Hila Peleg, Sorin Lerner, Nadia Polikarpova. FSE '21. pdf.

User-Guided Synthesis of Interactive Diagrams.

John Sarracino, Odaris Barrios-Arciga, Jasmine Zhu, Noah Marcus, Sorin Lerner, Ben Wiedermann. CHI '17. pdf, website, slides

Interactive Parser Synthesis by Example.

Alan Leung, John Sarracino, Sorin Lerner. PLDI '15. pdf.

JSAI: A Static Analysis Platform for JavaScript.

Vineeth Kashyap, Kyle Dewey, Ethan A. Kuefner, John Wagner, Kevin Gibbons, John Sarracino, Ben Wiedermann, Ben Hardekopf. FSE '14. pdf

Workshop Publications

Certified Parsing of Dependent Grammars.

John Sarracino, Gang Tan, Greg Morrisett. LangSec '22. code, pdf.

Chihuahua: A Concurrent, Moving, Garbage Collector using Transactional Memory.

Todd Anderson, Melissa O'Neil, John Sarracino. TRANSACT '15. pdf

Type Refinement for Static Analysis of JavaScript.

Vineeth Kashyap, John Sarracino, John Wagner, Ben Wiedermann, Ben Hardekopf. DLS '13. pdf


Targeted Synthesis for Programming with Data Invariants.

John Sarracino, Shraddha Barke, Hila Peleg, Sorin Lerner, Nadia Polikarpova. Arxiv '19. arxiv.

Professional Service

Program Committee

PLDI '24 '21, LangSec '21

External Review

ECOOP '23, OOPSLA '23 '22

Artifact Evaluation

ICFP '20, PLDI '20 '19 '18, ECOOP '23, OOPSLA '23 '22 '19 '18, CAV '19

Student Research Competition Committee


  1. Both authors contributed equally to this research.