Model Checking for Nominal Calculi
Ugo Montanari, Univ. Pisa, Italy
Location: George Square Lecture Theatre

Trace Partitioning in Abstract Interpretation Based Static Analyzers
Laurent Mauborgne and Xavier Rival (ENS, Paris, France)

Tool Paper: The ASTRÉE Analyzer
Patrick Cousot (ENS, Paris, France), Radhia Cousot (Ecole Polytechnique,, France), Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival (ENS, Paris, France)

Interprocedural Herbrand Equalities
Markus Müller-Olm (Univ. of Dortmund, Germany), Helmut Seidl (TU Munich, Germany) and Bernhard Steffen (Univ. of Dortmund, Germany)

Analysis of Modular Arithmetic
Markus Müller-Olm (Univ. of Dortmund, Germany) and Helmut Seidl (TU Munich, Germany)

Esterel v7: From Verified Formal Specification to Efficient Industrial Designs
Gérard Berry, Esterel Technologies, Villeneuve-Loubet, France
Location: George Square Lecture Theatre

Forward Slicing by Conjunctive Partial Deduction and Argument Filtering
Michael Leuschel (Univ. of Southampton, UK) and German Vidal (TU of Valencia, Spain)

A New Foundation For Control-Dependence and Slicing for Modern Program Structures
Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee (Kansas State Univ., Manhattan, USA), Matthew B. Dwyer (Univ. of Nebraska, Lincoln, USA) and John Hatcliff (Kansas State University, USA)

Summaries for While Programs with Recursion
Andreas Podelski, Ina Schaefer and Silke Wagner (MPI, Saarbrücken, Germany)

Determinacy Inference for Logic Programs
Lunjin Lu (Oakland Univ., Rochester, USA) and Andy King (Univ. of Kent, Canterbury, UK)

Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis
Oukseh Lee (Hanyang Univ., Ansan, Korea), Hongseok Yang and Kwangkeun Yi (Seoul National Univ., Korea)

Conference Dinner at the National Museum of Scotland, Chambers Street, preceded by a reception.

When you enter the museum, the first sight is the magnificent Main Hall, with its elegant bird-cage design. Flooded with natural light, it provides a great sense of space and tranquillity, with fountains and fishponds. It is a major exhibit in its own right and contains many wonderful objects.

During the dinner it will not be possible to see the exhibits of the museum, but here is what you will miss: Thirty-six galleries of varying sizes present artefacts from around the globe and natural history specimens. See everything from steamships to sculptures, Egypt to evolution, Dolly the Sheep to design classics and black holes to brown bears.

Programming with Explicit Security Policies
Andrew Myers, Cornell Univ., Ithaca, USA
Location: George Square Lecture Theatre

A Type Discipline for Authorization Policies
Cédric Fournet, Andrew Gordon and Sergio Maffeis (Microsoft Research, Cambridge, UK)

Computationally Sound, Automated Proofs for Security Protocols
Véronique Cortier (LORIA, Nancy, France) and Bogdan Warinschi (Univ. of California, Santa Cruz, USA)

Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries
Romain Janvier, Laurent Mazaré and Yassine Lakhnech (VERIMAG, Grenoble, France)

Analysis of an Electronic Voting Protocol in the Applied Pi Calculus
Steve Kremer (ENS Cachan, France) and Mark Ryan (Univ. of Birmingham, UK)

Streams with a Bottom in Functional Languages
Hideki Tsuiki and Keiji Sugihara (Kyoto Univ., Japan)

Bottom-up Beta-reduction: Uplinks and Lambda-DAGS
Olin Shivers (Georgia Institute of Technology, Atlanta, USA) and Mitchell Wand (Northeastern Univ., Boston, USA)

BI Hyperdoctrines and Higher Order Separation Logic
Bodil Biering, Lars Birkedal and Noah Torp-Smith (IT Univ. of Copenhagen, Denmark)

Deciding Reachability in Mobile Ambients
Nadia Busi and Gianluigi Zavattaro (Univ. of Bologna, Italy)

Denotational Semantics for Abadi and Leino's Logic of Objects
Bernhard Reus and Jan Schwinghammer (Univ. of Sussex, Brighton, UK)

A Design for a Security-typed Language with Certificate-based Declassification
Stephen Tse and Steve Zdancewic (Univ. of Pennsylvania, Philadelphia, USA)

Adjoining Declassification and Attack Models by Abstract Interpretation
Roberto Giacobazzi and Isabella Mastroeni (Univ. of Verona, Italy)

Enforcing Resource Bounds via Static Verification of Dynamic Checks
Ajay Chander, David Espinosa, Nayeem Islam (DoCoMo Labs, San José, USA), Peter Lee (Carnegie Mellon Univ., Pittsburgh, USA) and George Necula (Univ. of California, Berkeley, USA)

Asserting Bytecode Safety
Martin Wildmoser and Tobias Nipkow (TU Munich, Germany)

Subtyping First Class Polymorphic Components
João Costa Seco and Luís Caires (New Univ. of Lisbon, Portugal)

Complexity of Subtype Satisfiability over Posets
Joachim Niehren (INRIA Futurs, Lille, France), Tim Priesnitz (Saarland Univ., Saarbrücken, Germany) and Zhendong Su (Univ. of California, Davis, USA)

A Type System Equivalent to a Model Checker
Mayur Naik (Stanford Univ., USA) and Jens Palsberg (UCLA, USA)

Instant Polymorphic Type Systems for Mobile Process Calculi: Just Add Reduction Rules and Close
Henning Makholm and J. B. Wells (Heriot-Watt Univ., Edinburgh, UK)

Towards a Type System for Analyzing JavaScript Programs
Peter Thiemann (Univ. of Freiburg, Germany)

Java Jr: Fully Abstract Trace Semantics for a Core Java Language
Alan Jeffrey (Bell Labs, Lucent Technologies, Murray Hill, USA and DePaul Univ., Chicago, USA) and Julian Rathke (Univ. of Sussex, Brighton, UK)

Dinner at Jury's Inn, 43 Jeffrey Street. The hotel is perfectly located in the heart of the old city, right beside the Royal Mile.