| 2025 | CAV | Verifying Fault-Tolerance of Quantum Error Correction Codes. | Kean Chen, Yuhao Liu, Wang Fang, Jennifer Paykin, Xin-Chuan Wu, Albert T. Schmitz, Steve Zdancewic, Gushu Li |
| 2023 | CAV | Synthesizing Trajectory Queries from Examples. | Stephen Mell, Favyen Bastani, Steve Zdancewic, Osbert Bastani |
| 2023 | ECOOP | Semantics for Noninterference with Interaction Trees. | Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, Steve Zdancewic |
| 2023 | ITP | Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure. | Lawrence Dunn, Val Tannen, Steve Zdancewic |
| 2022 | ACL | Counterfactual Explanations for Natural Language Interfaces. | George Tolkachev, Stephen Mell, Steve Zdancewic, Osbert Bastani |
| 2021 | ISSTA | Model-based testing of networked applications. | Yishuai Li, Benjamin C. Pierce, Steve Zdancewic |
| 2021 | ITP | Verifying an HTTP Key-Value Server with Interaction Trees and VST. | Hengchu Zhang, Wolf Honor, Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, Steve Zdancewic |
| 2020 | CPP | An equational theory for weak bisimulation via generalized parameterized coinduction. | Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic |
| 2019 | CPP | From C to interaction trees: specifying, verifying, and testing a networked server. | Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honor, William Mansky, Benjamin C. Pierce, Steve Zdancewic |
| 2019 | SP | SoK: General Purpose Compilers for Secure Multi-Party Computation. | Marcella Hastings, Brett Hemenway, Daniel Noble, Steve Zdancewic |
| 2018 | ITP | A Formal Equational Theory for Call-By-Push-Value. | Christine Rizkallah, Dmitri Garbuzov, Steve Zdancewic |
| 2017 | CPP | Verifying dynamic race detection. | William Mansky, Yuanfeng Peng, Steve Zdancewic, Joseph Devietti |
| 2017 | HASKELL | The linearity Monad. | Jennifer Paykin, Steve Zdancewic |
| 2017 | POPL | QWIRE: a core language for quantum circuits. | Jennifer Paykin, Robert Rand, Steve Zdancewic |
| 2016 | POPL | Example-directed synthesis: a type-theoretic interpretation. | Jonathan Frankle, Peter-Michael Osera, David Walker, Steve Zdancewic |
| 2015 | CAV | An Axiomatic Specification for Sequential Memory Models. | William Mansky, Dmitri Garbuzov, Steve Zdancewic |
| 2015 | PLDI | A formal C memory model supporting integer-pointer casts. | Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis |
| 2015 | PLDI | Type-and-example-directed program synthesis. | Peter-Michael Osera, Steve Zdancewic |
| 2014 | CGO | WatchdogLite: Hardware-Accelerated Compiler-Based Pointer Checking. | Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic |
| 2014 | ESOP | A Core Quantitative Coeffect Calculus. | Alos Brunel, Marco Gaboardi, Damiano Mazza, Steve Zdancewic |
| 2014 | ICTAC | Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi. | Benot Valiron, Steve Zdancewic |
| 2013 | OOPSLA | Ironclad C++: a library-augmented type-safe subset of c++. | Christian DeLozier, Richard A. Eisenberg, Santosh Nagarakatte, Peter-Michael Osera, Milo M. K. Martin, Steve Zdancewic |
| 2013 | PLDI | Formal verification of SSA-based optimizations for LLVM. | Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic |
| 2012 | CPP | Mechanized Verification of Computing Dominators for Formalizing Compilers. | Jianzhou Zhao, Steve Zdancewic |
| 2012 | ISCA | Watchdog: Hardware for safe and secure manual memory management and full memory safety. | Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic |
| 2012 | POPL | Formalizing the LLVM intermediate representation for verified program transformations. | Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic |
| 2011 | POPL | Generative type abstraction and type-level computation. | Stephanie Weirich, Dimitrios Vytiniotis, Simon L. Peyton Jones, Steve Zdancewic |
| 2010 | APLAS | Relational Parametricity for a Polymorphic Linear Lambda Calculus. | Jianzhou Zhao, Qi Zhang, Steve Zdancewic |
| 2010 | ICFP | Lolliproc: to concurrency from classical linear logic via curry-howard and control. | Karl Mazurak, Steve Zdancewic |
| 2009 | CCS | Reactive noninterference. | Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjberg, Stephanie Weirich, Steve Zdancewic |
| 2009 | PLDI | Encoding information flow in Aura. | Limin Jia, Steve Zdancewic |
| 2009 | PLDI | SoftBound: highly compatible and complete spatial memory safety for c. | Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, Steve Zdancewic |
| 2008 | ASPLOS | Hardbound: architectural support for spatial safety of the C programming language. | Joe Devietti, Colin Blundell, Milo M. K. Martin, Steve Zdancewic |
| 2008 | ICFP | AURA: a programming language for authorization and audit. | Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, Steve Zdancewic |
| 2007 | PLDI | Combining events and threads for scalable network services implementation and evaluation of monadic, application-level concurrency primitives. | Peng Li, Steve Zdancewic |
| 2007 | POPL | Application-level concurrency: combining events and treads: invited talk. | Steve Zdancewic |
| 2007 | SP | A Cryptographic Decentralized Label Model. | Jeffrey A. Vaughan, Steve Zdancewic |
| 2006 | ICALP | Preserving Secrecy Under Refinement. | Rajeev Alur, Pavol Cern, Steve Zdancewic |
| 2005 | ESOP | A Design for a Security-Typed Language with Certificate-Based Declassification. | Stephen Tse, Steve Zdancewic |
| 2005 | POPL | Downgrading policies and relaxed noninterference. | Peng Li, Steve Zdancewic |
| 2004 | ICFP | Translating dependency into parametricity. | Stephen Tse, Steve Zdancewic |
| 2004 | SP | Run-time Principals in Information-flow Type Systems. | Stephen Tse, Steve Zdancewic |
| 2003 | ICFP | A theory of aspects. | David Walker, Steve Zdancewic, Jay Ligatti |
| 2003 | MFPS | A Type System for Robust Declassification. | Steve Zdancewic |
| 2003 | SP | Using Replication and Partitioning to Build Secure Distributed Systems. | Lantian Zheng, Stephen Chong, Andrew C. Myers, Steve Zdancewic |
| 2001 | ESOP | Secure Information Flow and CPS. | Steve Zdancewic, Andrew C. Myers |
| 2001 | SOSP | Untrusted Hosts and Confidentiality: Secure Program Partitioning. | Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, Andrew C. Myers |
| 1999 | ICFP | Principals in Programming Languages: A Syntactic Proof Technique. | Steve Zdancewic, Dan Grossman, J. Gregory Morrisett |