Bio

I'm a post-doc at Cornell, working with Greg Morrisett. My email address is jsarracino@cornell.edu. I defended my PhD at UCSD in 2020, working with Nadia Polikarpova and Sorin Lerner in the Programming Systems group.

My research interests lie at the intersection of Programming Languages (PL), Security, and Human-Computer Interaction (HCI). I'm interested in developing secure and robust systems using foundational verification, and broadening the impact and adoption of formal methods through proof engineering and language design.

Here are some of my current and past projects!

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



Publications

Conference Publications

Leapfrog: Certified Equivalence for Protocol Parsers

Ryan Doenges, Tobias Kappé, John Sarracino, Nate Foster, Greg Morrisett. Conditionally accepted to PLDI '22. 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, website

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 Regular Grammars.

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

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

Arxiv/Preprints

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 '21, LangSec '21

External Review

OOPSLA '22

Artifact Evaluation

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

Student Research Competition Committee

SPLASH '18


  1. Both authors contributed equally to this research.