| 2021 | ICTAC | A Complete Semantics of $\mathbb {K}$ and Its Translation to Isabelle. | Liyi Li, Elsa L. Gunter |
| 2020 | ECOOP | K-LLVM: A Relatively Complete Semantics of LLVM IR. | Liyi Li, Elsa L. Gunter |
| 2019 | CPP | Dynamic class initialization semantics: a jinja extension. | Susannah Mansky, Elsa L. Gunter |
| 2018 | SIGCSE | Using a Computer-based Testing Facility to Improve Student Learning in a Programming Languages and Compilers Course. | Terence Nip, Elsa L. Gunter, Geoffrey L. Herman, Jason W. Morphew, Matthew West |
| 2014 | ICTAC | Symbolic Analysis Tools for CSP. | Liyi Li, Elsa L. Gunter, William Mansky |
| 2012 | ITP | Using Locales to Define a Rely-Guarantee Temporal Logic. | William Mansky, Elsa L. Gunter |
| 2011 | ICFP | Recursion principles for syntax with bindings and substitution. | Andrei Popescu, Elsa L. Gunter |
| 2011 | ISSTA | Automated framework for formal operator task analysis. | Ayesha Yasmeen, Elsa L. Gunter |
| 2011 | SMC | Toward a multi-method approach to formalizing human-automation interaction and human-human communications. | Ellen J. Bass, Matthew L. Bolton, Karen M. Feigh, Dennis Griffith, Elsa L. Gunter, William Mansky, John M. Rushby |
| 2011 | SMC | Robustness for protection envelopes with respect to human task variation. | Ayesha Yasmeen, Elsa L. Gunter |
| 2010 | FOSSACS | Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization. | Andrei Popescu, Elsa L. Gunter |
| 2010 | ITP | A Framework for Formal Verification of Compiler Optimizations. | William Mansky, Elsa L. Gunter |
| 2010 | LICS | Strong Normalization for System F by HOAS on Top of FOAS. | Andrei Popescu, Elsa L. Gunter, Christopher J. Osborn |
| 2007 | RTSS | The Simplex Reference Model: Limiting Fault-Propagation Due to Unreliable Components in Cyber-Physical System Architectures. | Tanya L. Crenshaw, Elsa L. Gunter, Craig L. Robinson, Lui Sha, P. R. Kumar |
| 2006 | SMC | I-Living: An Open System Architecture for Assisted Living. | Qixin Wang, Wook Shin, Xue Liu, Zheng Zeng, Cham Oh, Bedoor K. AlShebli, Marco Caccamo, Carl A. Gunter, Elsa L. Gunter, Jennifer C. Hou, Karrie Karahalios, Lui Sha |
| 2002 | TACAS | Temporal Debugging for Concurrent Systems. | Elsa L. Gunter, Doron A. Peled |
| 2001 | TACAS | Compositional Message Sequence Charts. | Elsa L. Gunter, Anca Muscholl, Doron A. Peled |
| 2000 | CAV | PET: An Interactive Software Testing Tool. | Elsa L. Gunter, Robert P. Kurshan, Doron A. Peled |
| 2000 | PDPTA | Using a Mix of Languages in Formal Methods: The PET System. | Elsa L. Gunter, Doron A. Peled |
| 1999 | TACAS | Path Exploration Tool. | Elsa L. Gunter, Doron A. Peled |
| 1994 | DEXA | OR-SML: A Functional Database Programming Language for Disjunctive Information and Its Applications. | Elsa L. Gunter, Leonid Libkin |
| 1990 | CADE | Tutorial on Lambda-Prolog. | Amy P. Felty, Elsa L. Gunter, Dale Miller, Frank Pfenning |
| 1989 | MFPS | Pseudo-Retract Functors for Local Lattices and Bifinite L-domains. | Elsa L. Gunter |
| 1988 | CADE | Lambda-Prolog: An Extended Logic Programming Language. | Amy P. Felty, Elsa L. Gunter, John Hannan, Dale Miller, Gopalan Nadathur, Andre Scedrov |