Contact:
60 Fifth Avenue
Room 442
New York, NY 10011
(map)

About Me

I am a fifth year PhD student in computer science at the Courant Institute, New York University, working with Thomas Wies.

I am broadly interested in logic and formal verification. My current work focuses on implementability and synthesis of distributed protocols.

I received my B.S. (Hons) from Yale-NUS College, Singapore. Under the supervision of Aquinas Hobor and Frank Stephan, my capstone thesis formalized the theory of block pumpable languages in Coq.

Between Yale-NUS and NYU, I spent a year verifying blockchain consensus protocols at Runtime Verification.

Publications

  1. Sprout: A Verifier for Symbolic Multiparty Protocols
    Elaine Li, Felix Stutz, Thomas Wies and Damien Zufferey
    Under submission
  2. Characterizing Implementability of Global Protocols with Infinite States and Data
    Elaine Li, Felix Stutz, Thomas Wies and Damien Zufferey
    To appear at OOPSLA 2025
    PDF
  3. Deciding Subtyping for Asynchronous Multiparty Sessions
    Elaine Li, Felix Stutz, and Thomas Wies
    ESOP 2024
    PDF Slides
  4. Complete Multiparty Session Type Projection with Automata
    Elaine Li, Felix Stutz, Thomas Wies and Damien Zufferey
    CAV 2023
    PDF Slides
  5. Formalizing Correct-by-Construction Casper in Coq
    Elaine Li, Traian Serbanuta, Denisa Diaconescu, Vlad Zamfir, and Grigore Rosu
    ICBC 2020
    PDF Slides
  6. Pumping, With or Without Choice
    Aquinas Hobor, Elaine Li and Frank Stephan
    APLAS 2019
    PDF Slides Coq artifact
  7. Formalizing Block Pumpable Language Theory
    Elaine Li
    Yale-NUS College Capstone Thesis, 2019
    PDF Slides

Awards and Honors

NYU Courant Sandra Bleistein Prize
2024
NYU GSAS Dean's Dissertation Fellowship
2023
CAV VMW Scholarship
2023
NYU GSAS MacCracken Fellowship
2020-2025
Helmut Veith Scholarship (declined)
2019

Invited Talks

Implementability and Synthesis of Communication Protocols
  • Columbia University Systems seminar (February 2025)
  • Boston University POPV seminar (October 2024)
Synthesizing Distributed Protocols from Global Session Types
  • Simons Institute: Synthesis of Models and Systems (July 2024)
Multiparty Session Type Projection and Subtyping with Automata
  • UPenn PLClub (April 2024)
  • University of Luxembourg (April 2024)
  • Cornell PLDG (March 2024)
  • UCSC LSD seminar (October 2023)

Professional Activities

Program Committee
Dafny 2024
PLACES 2025
Subreviewer
FMCAD 2024