MONDAY
09.00 - 9.30: Welcome, etc
09.30 - 10.30: FIRST MORNING SESSION
ESOP Invited Lecture:
Resources, Concurrency and Local Reasoning
Peter O'Hearn, Queen Mary, University of London
10.30 - 11.00: coffee
11.00 - 12.30: SECOND MORNING SESSION
TACAS: THEOREM PROVING
Revisiting Positive Equality
Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur
An Interpolating Theorem Prover
Kenneth McMillan
Minimal Satisfying Assignments for Bounded Model Checking
Fabio Somenzi, Kavita Ravi
FASE: Objects and Aspects
Consistent Adaptation and Evolution of Class Diagrams during Refinement
Alexander Egyed (Teknowledge Corporation)
Measuring Aspect Cohesion
Jianjun Zhao (Fukuoka Institute of Technology), Baowen Xu (Southeast University)
Refactoring Object-Z Specifications
Tim McComb (The University of Queensland)
ESOP: Abstract Interpretation
Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors
Antoine Min\'e, Ecole Normale Sup\'erieure de Paris
Strong preservation as completeness in abstract interpretation
Francesco Ranzato and Francesco Tapparo, Universit\`a di Padova
Static Analysis of Digital Filters
J\'er\^ome Feret , Ecole Normale Sup\'erieure de Paris
12.30 - 14.30: LUNCH
14.30 - 16.00: FIRST AFTERNOON SESSION
TACAS: PROBABLISTIC MC
Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study
Håkan Younes, Marta Kwiatkowska, Gethin Norman, David Parker
Efficient computation of time-bounded reachability probabilities in
uniformized continuous-time Markov decision processes
Holger Hermanns, Christel Baier , Boudewijn R. Haverkort , Joost-Pieter Katoen
Model Checking Discounted Temporal Properties
Luca de Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga
FASE: Smart Cards
Checking Absence of Illicit Applet Interactions: A Case Study
Marieke Huisman (INRIA Sophia-Antipolis), Dilian Gurov (Royal
Institute of Technology Kista), Christoph Sprenger (INRIA Sophia-Antipolis),
Gennady Chugunov (Swedish Institute of Computer Science Kista)
A Tool-Assisted Framework for Certified Bytecode Verification
Gilles Barthe, Guillaume Dufay (INRIA Sophia-Antipolis)
Reasoning about Card Tears and Transactions in Java Card
Engelbert Hubbers, Erik Poll (University of Nijmegen)
ESOP: Modular and staged languages:
Sound and Decidable Type Inference for Functional Dependencies
Gregory J. Duck, University of Melbourne,Simon Peyton-Jones, Microsoft Research,
Peter J. Stuckey, University of Melbourne, and Martin Sulzmann, National
University of Singapore
Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types
Tom Hirschowitz, Ecole Normale Sup\'erieure de Lyon, Xavier Leroy,
INRIA Rocquencourt, and J. B. Wells, Heriot-Watt University
ML-like Inference for Classifiers
Cristiano Calcagno, Imperial College London, Eugenio Moggi,
Universit\'a di Genova, Walid Taha, Rice University
16.30 - 17.00: coffee
17.00 - 18.30: SECOND AFTERNOON SESSION
TACAS: TESTING
Automatic Creation of Environment Models via Training
Thomas Ball, Vladimir Levin, Fei Xie
Error Explanation with Distance Metrics
Alex Groce
Online Efficient Predictive Safety Analysis of Multithreaded Programs
Rosu, Grigore
Koushik Sen, Gul Agha
FASE: Components I
Predictable Dynamic Plugin Systems
Robert Chatley, Susan Eisenbach, Jeff Kramer, Jeff Magee, Sebastian
Uchitel (Imperial College London)
A Correlation Framework for the CORBA Component Model
Georg Jung, John Hatcliff, Venkatesh Prasad Ranganath (Kansas State
University)
Cadena: An Integrated Development Environment for Analysis, Synthesis,
and Verification of Component-based Systems
Adam Childs, Jesse Greenwald, Venkatesh Ranganath,
Xianghua Deng, Matthew Dwyer, John Hatcliff, Georg Jung, Prashant
Shanti, Gurdip Singh (Kansas State University)
ESOP: Constraint, logic, and pattern programming
From Constraints to Finite Automata to Filtering Algorithms
Mats Carlsson and Nicolas Beldiceanu,
Swedish Institute of Computer Science, Uppsala
A Memoizing Semantics for Functional Logic Languages
Espa{\~n}a-Boquera, Salvador Vicent Estruch
Technical University of Valencia
Adaptive Pattern Matching on Binary Data
Per Gustafsson and Konstantinos Sagonas, Uppsala University
TUESDAY
09.00 - 10.00: FIRST MORNING SESSION IS (Gruia)
FASE Invited Lecture:
A Formal Treatment of Context-Awareness
Gruia-Catalin Roman, Washington University
10.00 - 10.30: coffee
10.30 - 12.30: SECOND MORNING SESSION
TACAS: Tools
Vooduu: Verification of Object-Oriented Designs Using UPPAAL
Karsten Diethers, Michaela Huhn
CoPS - Checker of Persistent Security
Sabina Rossi, Carla Piazza, Enrico Pivato
Tampere Verification Tool
Henri Hansen, Heikki Virtanen, Henri Hansen, Antti Valmari,
Juha Nieminen, Timo Erkkilä
SyncGen: An Aspect-Oriented Framework for Automatically Generating
Synchronization Implementations from High-Level Specifications
John Hatcliff, Xianghua Deng, Matthew Dwyer, Masaaki Mizuno
MetaGame: An Animation Tool for Model-Checking Games
Markus Müller-Olm, Haiseung Yoo
A Tool for Checking ANSI-C Programs
Daniel Kroening, Edmund Clarke, Flavio Lerda
FASE: Security and Web Services
Actor-Centric Modeling of User Rights
Ruth Breu (Universität Innsbruck), Gerhard Popp (Technische
Universität München)
Modeling Role-Based Access Control Using Parameterized UML Models
Dae-Kyoo Kim, Indrakshi Ray, Robert France, Na Li (Colorado State
University)
Compositional Nested Long Running Transactions
Laura Bocchi (University of Bologna)
DaGen: A Tool for Automatic Translation from DAML-S to High-level Petri Nets
Daniel Moldt, Jan Ortmann (University of Hamburg)
ESOP: Spatial logics
Compositional Analysis of Authentication Protocols
Michele Bugliesi, Riccardo Focardi, and Matteo Maffei,
Univserit\`a C\'a Foscari di Venezia
A Distributed Abstract Machine for Boxed Ambient Calculi
Andrew Phillips, Nobuko Yoshida, and Susan Eisenbach,
Imperial College, London
A Dependently Typed Ambient Calculus
Cedric Lhoussaine and Vladimiro Sassone, University of Sussex
A Control Flow Analysis for Safe and Boxed Ambients
Francesca Levi, Universit\'a di Genova, and Chiara Bodei, Universit\`a di Pisa
12.30 - 14.30: LUNCH
14.30 - 16.30: FIRST AFTERNOON SESSION
FASE: Modeling and Requirements
Integrating Meta Modelling Aspects with Graph Transformation for
Efficient Visual Language Definition and Model Manipulation
Roswitha Bardohl, Hartmut Ehrig (Technische Universität Berlin),
Juan de Lara (Universidad Autónoma de Madrid), Gabriele
Taentzer (Technische Universität Berlin)
An Operational Semantics for Stateflow
Grégoire Hamon, John Rushby (SRI International)
Improving Use Case Based Requirements Using Formally Grounded Specifications
Christine Choppy (Université Paris XIII), Gianna Reggio (Università di
Genova)
The GOPCSD Tool: An Integrated Development Environment for Process
Control Requirements and Design
Islam A.M. El-Maddah, Tom S.E. Maibaum (King's College London)
ESOP: Distributed programming
Linear Types for Packet Processing
Robert Ennals, Intel Research,Richard Sharp and Alan Mycroft,
Cambridge University
Modal Proofs As Distributed Programs
Limin Jia and David Walker, Princeton University
ULM, A Core Programming Model for Global Computing
Gerard Boudol, INRIA, Sophia Antipolis
A Semantic Framework for Designer Transactions
Jan Vitek, Suresh Jagannathan, Adam Welc, Antony L. Hosking,
Purdue University
FOSSACS: Specification Formalisms
Partial Correctness Assertions Provable in Dynamic Logics
D. Leivant
Choice in Dynamic Linking
M. Abadi, G. Gonthier and B. Werner
Specifying and Verifying Partial Order Properties using Template MSCs
B. Genest, M. Minea, A. Muscholl and D. Peled
Reasoning about Dynamic Policies
R. Pucella and V. Weissman
16.30 - 17.00: coffee
17.00 - 18.30: SECOND AFTERNOON SESSION
TACAS: EXPLICITE STATE/PETRI NETS
Obtaining Memory-Efficient Reachability Graph Representations Using the
Sweep-Line Method
Michael Westergaard, Thomas Mailund
Automated generation of a progress measure for the sweep-line method
Karsten Schmidt
Tarjan's Algorithm Makes On-the-fly LTL Verification More Efficient
Jaco Geldenhuys, Antti Valmari
FASE: Testing
Automated Debugging using Path-Based Weakest Preconditions
Haifeng He, Neelam Gupta (The University of Arizona)
Filtering TOBIAS combinatorial test suites
Yves Ledru, Lydie du Bousquet, Olivier Maury, Pierre Bontron (IMAG)
Systematic Testing of Software Architectures in the C2 style
Henry Muccini (Università degli Studi dell'Aquila), Marcio
Dias (University of California at Irvine), D.J. Richardson
(University of California)
ESOP: Logics and typing
Semantical Analysis of Specification Logic, An Operational Approach
Dan Ghica, Oxford University
Answer Type Polymorphism in Call-by-name Continuation Passing
Hayo Thielecke, University of Birmingham
System E: Expansion Variables for Flexible Typing with Linear
and Non-linear Types and Intersection Types
Sebastian Carlier, Jeff Polakow, J. B. Wells, Heriot-Watt University,
and A. J. Kfoury, Boston University
WEDNESDAY
09.00 - 10.00: FIRST MORNING SESSION IS
ETAPS Invited Lecture:
***
Abiteboul
10.00 - 10.30: coffee
10.30 - 12.30: SECOND MORNING SESSION
FASE: Model Checking and Analysis
Optimising Communication Structure for Model Checking
Peter Saffrey (University College London), Muffy Calder (University of
Glasgow)
Translating Software Designs for Model Checking
Fei Xie (University of Texas at Austin), Vladimir Levin (Microsoft),
Robert P. Kurshan (Cadence), James C. Browne (University of Texas at
Austin)
Enhancing Remote Method Invocation through Type-Based Static Analysis
Carlo Ghezzi, Vincenzo Martena, Gian Pietro Picco (Politecnico di
Milano)
Specification and Analysis of Real-Time Systems Using Real-Time Maude
Peter Csaba Ölveczky (University of Illinois at Urbana-Champaign and
University of Oslo), José Meseguer (University of Illinois at
Urbana-Champaign)
ESOP: Security
A Hardest Attacker for Leaking References
Rene Rydhof Hansen, Technical University of Denmark
Trust Management in Strand Spaces: A Rely-Guarantee Method
Joshua Guttman, Javier Thayer, Jay Carlson, Jonathan Herzog,
John Ramsdell, Brian Sniffen, MITRE Corporation
Just Fast Keying in the Pi Calculus
Martin Abadi, University California Santa Cruz,
Bruno Blanchet, Ecole Normale Sup\'erieure de Paris and
Max-Institut f\"ur Informatik Saarbr\"ucken,
and C\'edric Fournet, Microsoft Research
Decidable Analysis of Cryptographic Protocols with Products and
Modular Exponentiation
Vitaly Shmatikov, SRI International
FOSSACS: Process Algebra and Distributed Computing
Election and Local Computations on Edges (Extended Abstract)
J. Chalopin and Y. Métivier
Finite Alphabets versus Omega-Completeness: From Ready Pairs to Ready Traces
W. Fokkink and S. Nain
Bisimulation on Speed: Lower Time Bounds
G. Lüttgen and W. Vogler
On the Expressiveness of CCS-like Calculi
P. Giambiagi, G. Schneider, and F.D. Valencia
12.30 - 14.30: LUNCH
14.30 - 15.30: FIRST AFTERNOON SESSION IS (Comon)
FOSSACS Invited Lecture:
***
Comon
15.30 - 16.30: SECOND AFTERNOON SESSION
TACAS: SCHEDULING
Resource-Optimal Scheduling Using Priced Timed Automata
Jacob Rasmussen, Kim G. Larsen, K. Subramani
Decidable and Undecidable Problems in Schedulability Analysis Using Timed
Automata
Yi Wang, Pavel Krcal
FASE: Components II
A Systematic Methodology for Developing Component Frameworks
Si Won Choi, Soo Ho Chang, Soo Dong Kim (Soongsil University)
Automating Decisions in Component Composition Based on Propagation of
Requirements
Ioana Sora, Vladimir Cretu (University Politehnica of Timisoara),
Pierre Verbaeten, Yolande Berbers (Katholieke Universiteit Leuven)
FOSSACS: Probabilistic Aspects
Perfect-information Stochastic Parity Games
W. Zielonka
Duality for Labelled Markov Processes
M. Mislove, J. Ouaknine, D. Pavlovic and J. Worrell
16.30 - 17.00: coffee
17.00 - 18.30: THIRD AFTERNOON SESSION
TACAS: CONSTRAINT SOLVING
The Succinct Solver Suite
Henrik Pilegaard, Flemming Nielson, Hanne Riis Nielson, Sun Hongyan, Mikael
René Buchholtz, Rydhof Hansen, Helmut Seidl
Binding-Time Analysis for MetaML via Type Inference and Constraint Solving
Nathan Linger, Tim Sheard
A Class of Polynomially Solvable Range Constraints for Interval Analysis
without Widenings and Narrowings
Zhendong Su, David Wagner
ESOP: Validation
Functors for Proofs and Programs
Jean-Christophe Filliatre and Pierre Letouzey, LRI-CNRS Universit\'e Paris-Sud
Extracting a Data Flow Analyser in Constructive Logic
David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu
IRISA and ENS Cachan
Canonical Graph Shapes
Arend Rensink, University of Twente
FOSSACS: Security
On the Existence of an Effective and Complete Inference System for
Cryptographic Protocols
L. Bozga, C. Ene and Y. Lakhnech,
A Note on the Perfect Encryption Assumption in a Process Calculus
P. Degano and R. Zunino,
Probabilistic Bisimulation and Equivalence for Security Analysis of
Network Protocols
A. Ramanathan, J. Mitchell, A. Scedrov and V. Teague
THURSDAY
09.00 - 10.00: FIRST MORNING SESSION IS (Valmari)
TACAS Invited Lecture:
What the Small Rubik's Cube Taught Me on Data Structures,
Information Theory and Randomisation
Antti Valmari, Tampere University of Technology (Finland)
10.00 - 10.30: coffee
10.30 - 12.30: SECOND MORNING SESSION
CC: Program Analysis
Analyzing memory accesses in x86 executables,
Gogul Balakrishnan and Thomas Reps, University of Wisconsin, Madison, USA.
The limits of alias analysis for scalar optimizations,
Rezaul A. Chowdhury, Peter Djeu, University of Texas, Austin, USA,
Brendon Cahoon, Conformative Systems, Austin, USA, James H. Burrill,
University of Massachusetts, Amherst, USA, and Kathryn S. McKinley,University of Texas, Austin, USA.
Pruning interference and ready dependence for slicing concurrent Java programs,
Venkatesh Prasad Ranganath and John Hatcliff, Kansas State University, USA.
Data dependence profiling for speculative optimizations,
Tong Chen, Jin Lin, Xiaorun Dai, Wei-Chung Hsu, and Pen-Chung Yew, University of Minnesota, USA.
TACAS: TIMED SYSTEMS
A Partial Order Semantics Approach to the Clock Explosion Problem of
Timed Automata
Peter Niebert, Sarah Zennou, Denis Lugiez
Lower and Upper Bounds in Zone Based Abstractions of Timed Automata
Gerd Behrmann, Patricia Bouyer, Kim G. Larsen, Radek Pelánek
A Scalable Incomplete Test for the Boundedness of UML RT Models
Stefan Leue, Richard Mayr, Wei Wei
Automatic Verification of Time-Sensitive Cryptographic Protocols
Giorgio Delzanno, Pierre Ganty
FOSSACS: Categorical Generalizations
Deriving Bisimulation Congruences in the DPO Approach to Graph Rewriting
H. Ehrig and B. Koenig
Adhesive Categories
S. Lack and P. Sobocinski
Canonical Models for Computational Effects
J. Power
Unifying Recursive and Co-recursive Definitions in Sheaf Categories
P. Di Gianantonio and M. Miculan
12.30 - 14.30: LUNCH
14.30 - 15.30: FIRST AFTERNOON SESSION
CC Invited Lecture:
***
Soffa
15.30 - 16.30: SECOND AFTERNOON SESSION
CC: Parsing
Elkhound: a fast, practical GLR parser generator,
Scott McPeak and George Necula, Berkeley, USA.
Generalised parsing: some engineering costs,
Adrian Johnstone, Elizabeth Scott, and Giorgios Economopoulos, University of London, UK.
TACAS: CASE STUDIES
Simulation-Based Verification of Autonomous Controllers with
Livingstone PathFinder
Tony Lindsey, Charles Pecheur
Automatic Parametric Verification of Root Contention Protocol based on
Abstract State Machines and First Order Timed Logic
Daniele Beauquier, Tristan Crolard, Evguenia Prokofieva
FOSSACS: Rewriting
Polynomials for Proving Termination of Context-Sensitive Rewriting
S. Lucas
On Term Rewriting Systems Having a Rational Derivation
A. Meyer
16.30 - 17.00: coffee
17.00 - 18.30: THIRD AFTERNOON SESSION
CC: Loop Analysis
An automata-theoretic algorithm for counting solutions to Presburger formulas,
Erin Parker, University of North Carolina, Chapel Hill, USA and
Siddhartha Chatterjee, IBM T.J.Watson Research Center, USA.
A symbolic approach to Bernstein expansion for program analysis and optimization,
Irina Tchoupaeva, Universite Strasbourg, France, and
Philippe Clauss, INRIA Rocquencourt, France.
Periodic polyhedra,
Benoît Meister, LSIIT-ICPS, Illkirch, France.
TACAS: SOFTWARE
Refining approximations in software predicate abstraction
Byron Cook, Thomas Ball, Satyaki Das, Sriram K. Rajamani
Checking Strong Specifications Using An Extensible Software Model-checking
Framework
Robby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff
Applying Game Semantics to Compositional Software Modeling and
Verification
Dan Ghica, Samson Abramsky, Andrzej Murawski, Luke Ong
FOSSACS: Automata Theory and Logic
Distance Desert Automata and the Star Height One Problem (Extended Abstract)
D. Kirsten
Tree Transducers and Tree Compressions
S. Maneth and G. Busatto
On Recognizable Timed Languages
O. Maler and A. Pnueli
LTL over Integer Periodicity Constraints (extended abstract)
S. Demri
FRIDAY
09.00 - 10.00: FIRST MORNING SESSION IS (Milner)
ETAPS Invited Lecture:
***
Milner
10.00 - 10.30: coffee
10.30 - 12.30: SECOND MORNING SESSION
CC: Optimization
Region-based partial dead code elimination on predicated code,
Qiong Cai, Lin Gao, Jingling Xue, University of New South Wales, Sydney, Australia.
Value-based partial redundancy elimination,
Thomas VanDrunen and Antony L. Hosking, Purdue University, USA.
Increasing the applicability of scalar replacement,
Byoungro So and Mary Hall, University of Southern California, USA.
Reducing the cost of object boxing,
Tim Owen and Des Watson, University of Sussex, Brighton, UK.
TACAS: TEMPORAL LOGIC
Solving disjunctive/conjunctive boolean equation systems with
alternating fixed points
Misa Keinänen, Jan Friso Groote,
How Vacuous is Vacuous?
Marsha Chechik, Arie Gurfinkel
A Temporal Logic of Nested Calls and Returns
P. Madhusudan, Rajeev Alur, Kousha Etessami
Liveness with Incomprehensible Ranking
Amir Pnueli, Yi Fang, Nir Piterman, Lenore Zuck
FOSSACS: Analysis of Computation
A Denotational Account of Untyped Normalization by Evaluation
A. Filinski and H.K. Rohde
Hypergraphs and Degrees of Parallelism: A Completeness Result
A. Bucciarelli and B. Leperchey
Strong normalization of lambda-bar-mu-mu-tilde-calculus with explicit
substitutions.
E. Polonovski
Soft Lambda-Calculus: A Language for Polynomial Time Computation
P. Baillot and V. Mogbil
12.30 - 14.30: LUNCH
14.30 - 16.30: FIRST AFTERNOON SESSION
CC: Code Generation and Backend Optimizations
FFT compiler techniques,
Stefan Kral, Franz Franchetti, Juergen Lorenz, Christoph W. Ueberhuber, and
Peter Wurzinger, Vienna University of Technology, Austria.
Widening integer arithmetic,
Kevin Redwine and Norman Ramsey, Harvard University, USA.
Stochastic bit-width approximation using Extreme Value Theory for customizable processors,
Emre Ozer, Andy P. Nisbet, David Gregg, Trinity College, Dublin, Ireland.
Using multiple memory access instructions for reducing code size,
Neil Johnson and Alan Mycroft, University of Cambridge, UK.
TACAS: ABSTRACTION
Guided Invariant Model Checking Based on Abstraction and Symbolic
Pattern Databases
Kairong Qian, Albert Nymeyer
Numerical Domains with Summarized Dimensions
Denis Gopan, Frank DiMaio, Nurit Dor, Thomas Reps, Mooly Sagiv
Symbolically Computing Most-Precise Abstract Operations for Shape
Analysis
Greta Yorsh, Thomas Reps, Mooly Sagiv
Monotonic Abstraction-Refinement for CTL
Orna Grumberg, Sharon Shoham
FOSSACS: Spatial Logics and Game Semantics
Decidability of Freshness, Undecidability of Revelation (Extended Abstract)
G. Conforti and G. Ghelli
Behavioral and Spatial Observations in a Logic for the Pi-Calculus
L. Caires
Angelic Semantics of Fine-Grained Concurrency
D.R. Ghica and A.S. Murawski
A Game Semantics of Local Names and Good Variables
J. Laird
16.30 - 17.00: coffee
17.00 - 18.30: SECOND AFTERNOON SESSION
CC: Compiler Construction
Integrating the Soot compiler infrastructure into an IDE,
Jennifer Lhotak, Ondrej Lhotak, and Laurie Hendren, McGill University, Montreal, Canada.
Declarative composition of stack frames,
Christian Lindig, Universitaet Saarbruecken, Germany and Norman Ramsey, Harvard University, USA.
TACAS: AUTOMATA TECHNIQUES
Omega-Regular Model Checking
Bernard Boigelot, Axel Legay, Pierre Wolper
FASTer acceleration of counter automata in practice
Bardin, Sebastien
Alain Finkel, Jerome Leroux
From Complementation to Certification
Moshe Vardi, Orna Kupferman
FOSSACS: Mobile Calculi
SAFEDPI: a language for controlling mobile code (Extended Abstract)
M. Hennessy, J. Rathke and N. Yoshida
Strong Bisimulation for the Explicit Fusion Calculus
L. Wischik and P. Gardner
Electoral Systems in Ambient Calculi
I. Phillips and M.G. Vigliotti