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