| 2005 | A bisimulation for type abstraction and recursion. | Eijiro Sumii, Benjamin C. Pierce |
| 2005 | Mutatis mutandis: safe and predictable dynamic software updating. | Gareth Paul Stoyle, Michael W. Hicks, Gavin M. Bierman, Peter Sewell, Iulian Neamtiu |
| 2005 | A variant of the Chaum voter-verifiable scheme. | Peter Y. A. Ryan |
| 2005 | A semantics for procedure local heaps and its abstractions. | Noam Rinetzky, Jrg Bauer, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm |
| 2005 | Transition predicate abstraction and fair termination. | Andreas Podelski, Andrey Rybalchenko |
| 2005 | A probabilistic language based upon sampling functions. | Sungwoo Park, Frank Pfenning, Sebastian Thrun |
| 2005 | Separation logic and abstraction. | Matthew J. Parkinson, Gavin M. Bierman |
| 2005 | From sequential programs to multi-tier applications by program transformation. | Matthias Neubauer, Peter Thiemann |
| 2005 | The Java memory model. | Jeremy Manson, William W. Pugh, Sarita V. Adve |
| 2005 | Downgrading policies and relaxed noninterference. | Peng Li, Steve Zdancewic |
| 2005 | Automated soundness proofs for dataflow analyses and transformations via local rules. | Sorin Lerner, Todd D. Millstein, Erika Rice, Craig Chambers |
| 2005 | Statically checking confidentiality via dynamic labels. | Bart Jacobs, Wolter Pieters, Martijn Warnier |
| 2005 | Parametric polymorphism for XML. | Haruo Hosoya, Alain Frisch, Giuseppe Castagna |
| 2005 | Using static analysis to validate the SAML single sign-on protocol. | Steffen M. Hansen, Jakob Skriver, Hanne Riis Nielson |
| 2005 | Region-based shape analysis with tracked locations. | Brian Hackett, Radu Rugina |
| 2005 | Precise interprocedural analysis using random interpretation. | Sumit Gulwani, George C. Necula |
| 2005 | Proof-guided underapproximation-widening for multi-process systems. | Orna Grumberg, Flavio Lerda, Ofer Strichman, Michael Theobald |
| 2005 | A framework for numeric analysis of array operations. | Denis Gopan, Thomas W. Reps, Shmuel Sagiv |
| 2005 | Formal prototyping in early stages of protocol design. | Alwyn Goodloe, Carl A. Gunter, Mark-Oliver Stehr |
| 2005 | A syntactic approach to eta equality in type theory. | Healfdene Goguen |
| 2005 | Slot games: a quantitative model of computation. | Dan R. Ghica |
| 2005 | Communicating quantum processes. | Simon J. Gay, Rajagopal Nagarajan |
| 2005 | Combinators for bi-directional tree transformations: a linguistic approach to the view update problem. | J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, Alan Schmitt |
| 2005 | Inferring authentication tags. | Riccardo Focardi, Matteo Maffei, Francesco Placella |
| 2005 | Dynamic partial-order reduction for model checking software. | Cormac Flanagan, Patrice Godefroid |