| 2005 | Trace Partitioning in Abstract Interpretation Based Static Analyzers. | Laurent Mauborgne, Xavier Rival |
| 2005 | Instant Polymorphic Type Systems for Mobile Process Calculi: Just Add Reduction Rules and Close. | Henning Makholm, J. B. Wells |
| 2005 | Determinacy Inference for Logic Programs. | Lunjin Lu, Andy King |
| 2005 | Forward Slicing by Conjunctive Partial Deduction and Argument Filtering. | Michael Leuschel, Germn Vidal |
| 2005 | Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis. | Oukseh Lee, Hongseok Yang, Kwangkeun Yi |
| 2005 | Analysis of an Electronic Voting Protocol in the Applied Pi Calculus. | Steve Kremer, Mark Ryan |
| 2005 | Java Jr: Fully Abstract Trace Semantics for a Core Java Language. | Alan Jeffrey, Julian Rathke |
| 2005 | Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries. | Romain Janvier, Yassine Lakhnech, Laurent Mazar |
| 2005 | Adjoining Declassification and Attack Models by Abstract Interpretation. | Roberto Giacobazzi, Isabella Mastroeni |
| 2005 | A Type Discipline for Authorization Policies. | Cdric Fournet, Andrew D. Gordon, Sergio Maffeis |
| 2005 | The ASTRE Analyzer. | Patrick Cousot, Radhia Cousot, Jrme Feret, Laurent Mauborgne, Antoine Min, David Monniaux, Xavier Rival |
| 2005 | Computationally Sound, Automated Proofs for Security Protocols. | Vronique Cortier, Bogdan Warinschi |
| 2005 | Enforcing Resource Bounds via Static Verification of Dynamic Checks. | Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee, George C. Necula |
| 2005 | Deciding Reachability in Mobile Ambients. | Nadia Busi, Gianluigi Zavattaro |
| 2005 | BI Hyperdoctrines and Higher-Order Separation Logic. | Bodil Biering, Lars Birkedal, Noah Torp-Smith |
| 2004 | A Semantic Framework for Designer Transactions. | Jan Vitek, Suresh Jagannathan, Adam Welc, Antony L. Hosking |
| 2004 | Answer Type Polymorphism in Call-by-Name Continuation Passing. | Hayo Thielecke |
| 2004 | Decidable Analysis of Cryptographic Protocols with Products and Modular Exponentiation. | Vitaly Shmatikov |
| 2004 | Canonical Graph Shapes. | Arend Rensink |
| 2004 | Strong Preservation as Completeness in Abstract Interpretation. | Francesco Ranzato, Francesco Tapparo |
| 2004 | A Distributed Abstract Machine for Boxed Ambient Calculi. | Andrew Phillips, Nobuko Yoshida, Susan Eisenbach |
| 2004 | Resources, Concurrency, and Local Reasoning (Abstract). | Peter W. O'Hearn |
| 2004 | Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors. | Antoine Min |
| 2004 | A Dependently Typed Ambient Calculus. | Cdric Lhoussaine, Vladimiro Sassone |
| 2004 | A Control Flow Analysis for Safe and Boxed Ambients. | Francesca Levi, Chiara Bodei |