| 2005 | A Design for a Security-Typed Language with Certificate-Based Declassification. Stephen Tse, Steve Zdancewic |
| 2005 | A New Foundation for Control-Dependence and Slicing for Modern Program Structures. Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee, Matthew B. Dwyer, John Hatcliff |
| 2005 | A Type Discipline for Authorization Policies. Cédric Fournet, Andrew D. Gordon, Sergio Maffeis |
| 2005 | A Type System Equivalent to a Model Checker. Mayur Naik, Jens Palsberg |
| 2005 | Adjoining Declassification and Attack Models by Abstract Interpretation. Roberto Giacobazzi, Isabella Mastroeni |
| 2005 | Analysis of Modular Arithmetic. Markus Müller-Olm, Helmut Seidl |
| 2005 | Analysis of an Electronic Voting Protocol in the Applied Pi Calculus. Steve Kremer, Mark Ryan |
| 2005 | Asserting Bytecode Safety. Martin Wildmoser, Tobias Nipkow |
| 2005 | Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis. Oukseh Lee, Hongseok Yang, Kwangkeun Yi |
| 2005 | BI Hyperdoctrines and Higher-Order Separation Logic. Bodil Biering, Lars Birkedal, Noah Torp-Smith |
| 2005 | Bottom-Up beta-Reduction: Uplinks and lambda-DAGs. Olin Shivers, Mitchell Wand |
| 2005 | Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries. Romain Janvier, Yassine Lakhnech, Laurent Mazaré |
| 2005 | Complexity of Subtype Satisfiability over Posets. Joachim Niehren, Tim Priesnitz, Zhendong Su |
| 2005 | Computationally Sound, Automated Proofs for Security Protocols. Véronique Cortier, Bogdan Warinschi |
| 2005 | Deciding Reachability in Mobile Ambients. Nadia Busi, Gianluigi Zavattaro |
| 2005 | Denotational Semantics for Abadi and Leino's Logic of Objects. Bernhard Reus, Jan Schwinghammer |
| 2005 | Determinacy Inference for Logic Programs. Lunjin Lu, Andy King |
| 2005 | Enforcing Resource Bounds via Static Verification of Dynamic Checks. Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee, George C. Necula |
| 2005 | Forward Slicing by Conjunctive Partial Deduction and Argument Filtering. Michael Leuschel, Germán Vidal |
| 2005 | Instant Polymorphic Type Systems for Mobile Process Calculi: Just Add Reduction Rules and Close. Henning Makholm, J. B. Wells |
| 2005 | Interprocedural Herbrand Equalities. Markus Müller-Olm, Helmut Seidl, Bernhard Steffen |
| 2005 | Java Jr: Fully Abstract Trace Semantics for a Core Java Language. Alan Jeffrey, Julian Rathke |
| 2005 | Programming Languages and Systems, 14th European Symposium on Programming, ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings Shmuel Sagiv |
| 2005 | Programming with Explicit Security Policies. Andrew C. Myers |
| 2005 | Streams with a Bottom in Functional Languages. Hideki Tsuiki, Keiji Sugihara |
| 2005 | Subtyping First-Class Polymorphic Components. João Costa Seco, Luís Caires |
| 2005 | Summaries for While Programs with Recursion. Andreas Podelski, Ina Schaefer, Silke Wagner |
| 2005 | The ASTREÉ Analyzer. Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival |
| 2005 | Towards a Type System for Analyzing JavaScript Programs. Peter Thiemann |
| 2005 | Trace Partitioning in Abstract Interpretation Based Static Analyzers. Laurent Mauborgne, Xavier Rival |