| 2024 | ASPLOS | Avoiding Instruction-Centric Microarchitectural Timing Channels Via Binary-Code Transformations. | Michael Flanders, Reshabh K. Sharma, Alexandra E. Michael, Dan Grossman, David Kohlbrenner |
| 2024 | ITP | Correctly Compiling Proofs About Programs Without Proving Compilers Correct. | Audrey Seo, Christopher Lam, Dan Grossman, Talia Ringer |
| 2024 | SP | Defending Language Models Against Image-Based Prompt Attacks via User-Provided Specifications. | Reshabh K. Sharma, Vinayak Gupta, Dan Grossman |
| 2021 | PLDI | Proof repair across type equivalences. | Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, Dan Grossman |
| 2021 | PLDI | Reticle: a virtual machine for programming modern FPGAs. | Luis Vega, Joseph McMahan, Adrian Sampson, Dan Grossman, Luis Ceze |
| 2020 | CPP | REPLica: REPL instrumentation for Coq analysis. | Talia Ringer, Alex Sanchez-Stern, Dan Grossman, Sorin Lerner |
| 2020 | PLDI | Synthesizing structured CAD models with equality saturation and inverse transformations. | Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman, Zachary Tatlock |
| 2019 | ITP | Ornaments for Proof Reuse in Coq. | Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman |
| 2018 | CPP | Œuf: minimizing the Coq extraction TCB. | Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman |
| 2018 | CPP | Adapting proof automation to adapt proofs. | Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman |
| 2018 | ECOOP | Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates. | John Toman, Dan Grossman |
| 2017 | PLDI | Debugging probabilistic programs. | Chandrakana Nandi, Dan Grossman, Adrian Sampson, Todd Mytkowicz, Kathryn S. McKinley |
| 2016 | CCS | AUDACIOUS: User-Driven Access Control with Unmodified Operating Systems. | Talia Ringer, Dan Grossman, Franziska Roesner |
| 2016 | ECOOP | Staccato: A Bug Finder for Dynamic Configuration Updates. | John Toman, Dan Grossman |
| 2016 | PLDI | Verified peephole optimizations for CompCert. | Eric Mullen, Daryl Zuniga, Zachary Tatlock, Dan Grossman |
| 2016 | POPL | Optimizing synthesis with metasketches. | James Bornholt, Emina Torlak, Dan Grossman, Luis Ceze |
| 2015 | ASPLOS | Monitoring and Debugging the Quality of Results in Approximate Programs. | Michael F. Ringenburg, Adrian Sampson, Isaac Ackerman, Luis Ceze, Dan Grossman |
| 2015 | OOPSLA | Probability type inference for flexible approximate programming. | Brett Boston, Adrian Sampson, Dan Grossman, Luis Ceze |
| 2015 | SIGCSE | SPOCs: What, Why, and How. | Janet E. Burge, Armando Fox, Dan Grossman, Gerald Roth, Joe Warren |
| 2014 | ASPLOS | Low-level detection of language-level data races with LARD. | Benjamin P. Wood, Luis Ceze, Dan Grossman |
| 2014 | ICSE | How programming languages will co-evolve with software engineering: a bright decade ahead. | Emerson R. Murphy-Hill, Dan Grossman |
| 2014 | OOPSLA | Symbolic execution of multithreaded programs from arbitrary program contexts. | Tom Bergan, Dan Grossman, Luis Ceze |
| 2014 | PLDI | Test-driven synthesis. | Daniel Perelman, Sumit Gulwani, Dan Grossman, Peter Provost |
| 2014 | PLDI | Expressing and verifying probabilistic assertions. | Adrian Sampson, Pavel Panchekha, Todd Mytkowicz, Kathryn S. McKinley, Dan Grossman, Luis Ceze |
| 2013 | ECOOP | Java UI : Effects for Controlling UI Object Access. | Colin S. Gordon, Werner Dietl, Michael D. Ernst, Dan Grossman |
| 2013 | OOPSLA | Input-covering schedules for multithreaded programs. | Tom Bergan, Luis Ceze, Dan Grossman |
| 2013 | PLDI | Rely-guarantee references for refinement types over aliased mutable data. | Colin S. Gordon, Michael D. Ernst, Dan Grossman |
| 2012 | DLS | Detecting conflicts among declarative UI extensions. | Benjamin S. Lerner, Dan Grossman |
| 2012 | ISCA | RADISH: Always-on sound and complete race detection in software and hardware. | Joseph Devietti, Benjamin P. Wood, Karin Strauss, Luis Ceze, Dan Grossman, Shaz Qadeer |
| 2012 | OOPSLA | IFRit: interference-free regions for dynamic data-race detection. | Laura Effinger-Dean, Brandon Lucia, Luis Ceze, Dan Grossman, Hans-Juergen Boehm |
| 2012 | PLDI | Type-directed completion of partial expressions. | Daniel Perelman, Sumit Gulwani, Thomas Ball, Dan Grossman |
| 2012 | SIGCSE | Introducing parallelism and concurrency in the data structures course. | Dan Grossman, Ruth E. Anderson |
| 2011 | ASPLOS | RCDC: a relaxed consistency deterministic computer. | Joseph Devietti, Jacob Nelson, Tom Bergan, Luis Ceze, Dan Grossman |
| 2011 | PLDI | EnerJ: approximate data types for safe and general low-power computation. | Adrian Sampson, Werner Dietl, Emily Fortuna, Danushen Gnanapragasam, Luis Ceze, Dan Grossman |
| 2011 | PLDI | Data-race exceptions have benefits beyond the memory model. | Benjamin P. Wood, Luis Ceze, Dan Grossman |
| 2010 | ASPLOS | CoreDet: a compiler and runtime system for deterministic multithreaded execution. | Tom Bergan, Owen Anderson, Joseph Devietti, Luis Ceze, Dan Grossman |
| 2010 | ICDE | Estimating the progress of MapReduce pipelines. | Kristi Morton, Abram L. Friesen, Magdalena Balazinska, Dan Grossman |
| 2010 | MICRO | ASF: AMD64 Extension for Lock-Free Data Structures and Transactional Memory. | Jae-Woong Chung, Luke Yen, Stephan Diestelhorst, Martin Pohlack, Michael Hohmuth, David Christie, Dan Grossman |
| 2010 | OOPSLA | Supporting dynamic, third-party code customizations in JavaScript using aspects. | Benjamin S. Lerner, Herman Venter, Dan Grossman |
| 2010 | OOPSLA | Composable specifications for structured shared-memory communication. | Benjamin P. Wood, Adrian Sampson, Luis Ceze, Dan Grossman |
| 2010 | SIGMOD | ParaTimer: a progress indicator for MapReduce DAGs. | Kristi Morton, Magdalena Balazinska, Dan Grossman |
| 2008 | CC | Automatic Transformation of Bit-Level C Code to Support Multiple Equivalent Data Layouts. | Marius Nita, Dan Grossman |
| 2008 | ICFP | Transactional events for ML. | Laura Effinger-Dean, Matthew Kehrt, Dan Grossman |
| 2008 | POPL | High-level small-step operational semantics for transactions. | Katherine F. Moore, Dan Grossman |
| 2008 | POPL | A theory of platform-dependent low-level software. | Marius Nita, Dan Grossman, Craig Chambers |
| 2007 | ICSE | Automatic Inference of Structural Changes for Matching across Program Versions. | Miryung Kim, David Notkin, Dan Grossman |
| 2007 | OOPSLA | The transactional memory / garbage collection analogy. | Dan Grossman |
| 2007 | PLDI | Searching for type-error messages. | Benjamin S. Lerner, Matthew Flower, Dan Grossman, Craig Chambers |
| 2007 | PLDI | Enforcing isolation and ordering in STM. | Tatiana Shpeisman, Vijay Menon, Ali-Reza Adl-Tabatabai, Steven Balensiefer, Dan Grossman, Richard L. Hudson, Katherine F. Moore, Bratin Saha |
| 2005 | CCS | Preventing format-string attacks via automatic and efficient dynamic checking. | Michael F. Ringenburg, Dan Grossman |
| 2005 | ICFP | AtomCaml: first-class atomicity via rollback. | Michael F. Ringenburg, Dan Grossman |
| 2002 | ESOP | Existential Types for Imperative Languages. | Dan Grossman |
| 2002 | PLDI | Region-Based Memory Management in Cyclone. | Dan Grossman, J. Gregory Morrisett, Trevor Jim, Michael W. Hicks, Yanling Wang, James Cheney |
| 2002 | USENIX | Cyclone: A Safe Dialect of C. | Trevor Jim, J. Gregory Morrisett, Dan Grossman, Michael W. Hicks, James Cheney, Yanling Wang |
| 1999 | ICFP | Principals in Programming Languages: A Syntactic Proof Technique. | Steve Zdancewic, Dan Grossman, J. Gregory Morrisett |
| 1999 | SIGCSE | JDuck: building a software engineering tool in Java as a CS2 project. | Michael W. Godfrey, Dan Grossman |