I am a programming languages and applied formal methods researcher.
My recent work is on certified systems in Coq and making Coq proofs easier.
I am broadly interested in the application of PL/FM to networking,
systems, and security; and on easing the burden of certified programming.
I'm currently consulting for the Cloud and Software Security group at Bloomberg LP, working on formalizing low-level systems code in Coq. My email address is email@example.com.
Before this, I had the pleasure of doing a postdoc with Greg Morrisett at Greg Morrisett at Cornell and a PhD at UCSD with Nadia Polikarpova and Sorin Lerner in the Programming Systems group.
Here are some of my current and past projects!
- 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.
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 Sarracino, Dylan Lukes, 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
Vineeth Kashyap, Kyle Dewey, Ethan A. Kuefner, John Wagner, Kevin Gibbons, John Sarracino, Ben Wiedermann, Ben Hardekopf.
FSE '14. pdf
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
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.
PLDI '21, LangSec '21
ECOOP '23, OOPSLA '23 '22
ICFP '20, PLDI '20 '19 '18, ECOOP '23, OOPSLA '23 '22 '19 '18, CAV '19
Student Research Competition Committee