| 2006 | Modular set-based analysis from contracts. | Philippe Meunier, Robert Bruce Findler, Matthias Felleisen |
| 2006 | A verifiable SSA program representation for aggressive compiler optimization. | Vijay Menon, Neal Glew, Brian R. Murphy, Andrew McCreight, Tatiana Shpeisman, Ali-Reza Adl-Tabatabai, Leaf Petersen |
| 2006 | Why dependent types matter. | James McKinna |
| 2006 | Autolocker: synchronization inference for atomic sections. | Bill McCloskey, Feng Zhou, David Gay, Eric A. Brewer |
| 2006 | Protecting representation with effect encapsulation. | Yi Lu, John Potter |
| 2006 | Interruptible iterators. | Jed Liu, Aaron Kimball, Andrew C. Myers |
| 2006 | Formal certification of a compiler back-end or: programming a compiler with a proof assistant. | Xavier Leroy |
| 2006 | Verifying properties of well-founded linked lists. | Shuvendu K. Lahiri, Shaz Qadeer |
| 2006 | Small bisimulations for reasoning about higher-order imperative programs. | Vasileios Koutavas, Mitchell Wand |
| 2006 | A polymorphic modal type system for lisp-like multi-staged languages. | Ik-Soon Kim, Kwangkeun Yi, Cristiano Calcagno |
| 2006 | On flow-sensitive security types. | Sebastian Hunt, David Sands |
| 2006 | Simplifying reductions. | Gautam Gupta, Sanjay V. Rajopadhye |
| 2006 | Hybrid type checking. | Cormac Flanagan |
| 2006 | The next 700 data description languages. | Kathleen Fisher, Yitzhak Mandelbaum, David Walker |
| 2006 | A virtual class calculus. | Erik Ernst, Klaus Ostermann, William R. Cook |
| 2006 | Harmless advice. | Daniel S. Dantas, David Walker |
| 2006 | Adventures in time and space. | Norman Danner, James S. Royer |
| 2006 | Fast and loose reasoning is morally correct. | Nils Anders Danielsson, John Hughes, Patrik Jansson, Jeremy Gibbons |
| 2006 | Decidability and proof systems for language-based noninterference relations. | Mads Dam |
| 2006 | Untitled record | Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, Marc Pouzet |
| 2006 | Compiler-directed channel allocation for saving power in on-chip networks. | Guangyu Chen, Feihui Li, Mahmut T. Kandemir |
| 2006 | Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations. | Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough |
| 2006 | A logic for information flow in object-oriented programs. | Torben Amtoft, Sruthi Bandhakavi, Anindya Banerjee |
| 2006 | A fixpoint calculus for local and global program flows. | Rajeev Alur, Swarat Chaudhuri, P. Madhusudan |
| 2005 | Scalable error detection using boolean satisfiability. | Yichen Xie, Alex Aiken |