Shaan Nagy

NSF Graduate Research Fellow, UCSD
  • (2024) M.S. in CS from UW–Madison
  • (2022) B.S. in Math & CS from Rice



Who am I?

I am a fourth-year Computer Science PhD student at UCSD working under Loris D’Antoni. My recent work has focused on semantics and verification over infinite sets of programs. In general, I am interested in using denotational semantics to define metatheories of program analysis. I am also interested in developing novel program analyses to enable principled code generation.

I received my BSCS in Computer Science and BS in Math from Rice University in May 2022. While there, I worked with Moshe Vardi on computing partition functions of Ising models.

If you are a UCSD undergrad/master’s student interested in my research and looking for ways to get involved, feel free to write some pruners in ChopChop and reach out!


Publications

  • [POPL 26] ChopChop: a programmable framework for semantically constraining the output of language models. Nagy, S.*, Zhou, T.*, Polikarpova, N., & D'Antoni, L. *Equal contribution [paper][code]

  • [OOPSLA 25] Semantics of sets of programs. Kim, J.*, Nagy, S.*, Reps, T., & D’Antoni, L. *Equal contribution [paper][slides(pdf)][slides(pptx)]

  • [OOPSLA 24] Automating unrealizability logic: Hoare-style proof synthesis for infinite sets of programs. Nagy, S., Kim, J., D’Antoni, L., & Reps, T. [paper][code][slides(pdf)][slides(pptx)]

  • [PRE 24] Ising model partition function computation as a weighted counting problem. Nagy, S., Paredes, R., Dudek, J. M., Dueñas-Osorio, L., & Vardi, M. Y. [paper][code]


Awards

UCSD
  • NSF Graduate Research Fellowship Awardee [National Science Foundation] (2024)
UW-Madison
  • First Year Summer Research Assistantship Award (2023)
Rice University
  • Summa cum Laude (CS)/Magna cum Laude (Math) (2022)
  • Phi Beta Kappa (2022)
  • Louis J. Walsh Engineering Scholarship (2020)


Speaking

Talks
  • In Search of Failed Search: Unrealizability for Program Synthesis, SoCal PLS, 2026
  • Semantics of Sets of Programs, OOPSLA, 2025
  • Automated Switch Validation with Path-Complete Testing at Scale, P4 Workshop, 2024 [link]
  • Hoare-style Proof Synthesis for Infinite Sets of Programs: Automating Unrealizability Logic, OOPSLA, 2024
Lectures
  • Program Verification, (Guest Lecture) CS 538: Introduction to Programming Languages, UW-Madison, April 22, 2024
  • LR Parsing, (Substitute Lecture) CS 536: Introduction to Programming Languages and Compilers, UW-Madison, March 9, 2023
Posters
  • ChopChop: a programmable framework for semantically constraining the output of language models. Nagy, S.*, Zhou, T.*, Polikarpova, N., & D'Antoni, L. *Equal contribution at DL4C workshop @ Neurips, 2025[pdf]
  • Hoare-style Proof Synthesis for Infinite Sets of Programs: Automating Unrealizability Logic. Nagy, S., Kim, J., D’Antoni, L., & Reps, T. at OOPSLA, 2024 [pdf]