MONDAY

MONDAY 9:00-9:30 Opening
Central Hall

MONDAY 9:30-10:30 Invited Speaker
Central Hall, Chair: Oege de Moor / Michael Schwartzbach

Challenges in Code Optimization of Parallel Programs

Vivek Sarkar (Rice University)

 

10.30-11.00 Coffee (Exhibition Centre)

 

MONDAY 11:00-12:30 (3 parallel 3-paper sessions)

CC - Formal Properties of Optimisations
Room P/L002, Chair: Sorin Lerner

• Extensible Proof-Producing Compilation
  Magnus O. Myreen (University of Cambridge), Konrad Slind (University of Utah) and Mike Gordon (University of Cambridge)
• An Architecture for Safe Optimisation of Java Bytecode
  Richard Warburton (University of Warwick) and Sara Kalvala (University of Warwick)
• A Framework for Exploring Optimization Properties
  Min Zhao (University of Pittsburgh), Bruce Childers (University of Pittsburgh) and Mary Lou Soffa (University of Virginia)

FOSSACS - Semantics
Room P/L001, Chair: Roberto Amadio

• Least and Greatest Fixpoints in Game Semantics
  Pierre Clairambault (Université Paris 7)
• Full Abstraction for Reduced ML
  Andrzej Murawski (Oxford University) and Nikos Tzevelekos (Oxford University)
• Logics and Bisimulation Games for Concurrency, Causality and Conflict
  Julian Gutierrez (University of Edinburgh)

TACAS - Model Checking I
Room P/X001, Chair: Luca de Alfaro

• Hierachical Set Decision Diagrams & Regular Models
  Yann Thierry-Mieg (Université P. & M. Curie), Denis Poitrenaud (Université P. & M. Curie), Alexandre Hamez (Université P. & M. Curie) and Fabrice Kordon (Université P. & M. Curie)
• Büchi Complementation and Size-Change Termination
  Seth Fogarty (Rice University) and Moshe Vardi (Rice University)
• Learning Minimal Separating DFAs for Compositional Verification
  Yu-Fang Chen (National Taiwan University), Azadeh Farzan (University of Toronto), Edmund Clarke (Carnegie Mellon University), Yih-Kuen Tsay (National Taiwan University) and Bow-Yaw Wang (Academia Sinica)

 

12.30-14.30 Lunch (Roger Kirk Centre)

 

MONDAY 14:30-16:30 (3 parallel 4-paper sessions)

CC - Concurrency and Distributed Systems
Room P/L002 , Chair: Satish Chandra

• Compile-Time Analysis and Specialization of Clocks in Concurrent Programs
  Nalini Vasudevan (Columbia University), Olivier Tardieu (IBM T.J.Watson Research Center), Julian Dolby (IBM T.J. Watson Research Center) and Stephen A. Edwards (Columbia University)
• Implementation and Use of Transactional Memory with Dynamic Separation
  Martin Abadi (UCSC and Microsoft), Andrew Birrell (Microsoft Research), Tim Harris (Microsoft Research), Johnson Hsieh (Microsoft Research) and Michael Isard (Microsoft Research)
• Exploiting Speculative TLP in Recursive Programs by Dynamic Thread Prediction
  Lin Gao (University of New South Wales), Lian Li (University of New South Wales), Jingling Xue (University of New South Wales) and Tin-Fook Ngai (Microprocessor Technology Lab, Intel)
• Live Debugging of Distributed Systems
  Darren Dao (University of California, San Diego), Jeannie Albrecht (Williams College), Charles Killian (Purdue University) and Amin Vahdat (University of California, San Diego)

FOSSACS - Logics and Automata
Room P/L001, Chair: Parosh Abdullah

• Separating Graph Logic from MSO
  Timos Antonopoulos (University of Cambridge) and Anuj Dawar (University of Cambridge)
• The Completeness of First-Order Dynamic Logic
  Daniel Leivant (Indiana University)
• Dependency Tree Automata
  Colin Stirling (University of Edinburgh)
• On Global Model Checking Trees Generated by Higher-Order Recursion Schemes
  Christopher Broadbent (Oxford University) and Luke Ong (Oxford University)

TACAS - Tools I
Room P/X001, Chair: Carsten Weise

• RBAC-PAT: A Policy Analysis Tool for Role Based Access Control
  Mikhail Gofman (Binghampton University), Ruiqi Luo (Binghampton University), Ayla Solomon (Wellesley College), Yingbin Zhang (Binghampton University), Ping Yang (Binghampton University) and Scott Stoller (Stony Brook University)
• ITPN-PerfBound: A Performance Bound Tool for Interval Time Petri Nets
  Elina Pacini Naumovich (Università di Torino), Simona Bernardi (Università di Torino) and Marco Gribaudo (Università di Torino)
• Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches
  Didier Lime (IRCCyN, CNRS), Olivier Roux (IRCCyN, CNRS), Charlotte Seidner (IRCCyN, CNRS) and Louis-Marie Traonouez (IRCCyN, CNRS)
• Alpaga: A Tool for Solving Parity Games with Imperfect Information
  Dietmar Berwanger (LSV, ENS Cachan and CNRS), Krishnendu Chatterjee (University of California, Santa Cruise), Martin De Wulf (Université Libre de Bruxelles), Laurent Doyen (École Polytechnique Fédérale de Lausanne) and Thomas Henzinger (École Polytechnique Fédérale de Lausanne)

 

16.30-17.00 Coffee (Exhibition Centre)

 

MONDAY 17:00-18:30 (3 parallel 3-paper sessions)

CC - Frontend Technology
Room P/L002, Chair: Michael Schwartzbach

• Parsing C/C++ Code without Preprocessing
  Yoann Padioleau (University of Urbana Champaign)
• Faster Scannerless GLR Parsing
  Giorgios Economopoulos (University of Southampton), Paul Klint (Centrum voor Wiskunde en Informatica) and Jurgen Vinju (Centrum voor Wiskunde en Informatica)
• Decorated Attribute Grammars { Attribute Evaluation meets Strategic Programming
  Lennart C. L. Kats (Delft University of Technology), Tony Sloane (Macquarie University) and Eelco Visser (Delft University of Technology)

FOSSACS - Algebras
Room P/L001, Chair: Grigore Rosu

• A Kleene Theorem for Polynomial Coalgebras
  Marcello Bonsangue (CWI, Netherlands), Jan Rutten (CWI, Netherlands) and Alexandra Silva (CWI, Netherlands)
• Coalgebraic Hybrid Logic
  Robert Myers (Imperial College), Dirk Pattinson (Imperial College) and Lutz Schröder (DFKI Bremen and Universität Bremen)
• A Description of Iterative Reflections of Monads
  Jiri Adamek (Technical University of Brauschweig), Stefan Milius (Technical University of Brauschweig) and Jiri Velebil (Czech Technical University)

TACAS - Game-theoretic Approaches
Room P/X001, Chair: Michael Huth

• Compositional Predicate Abstraction from Game Semantics
  Adam Bakewell (University of Birmingham) and Dan Ghica (University of Birmingham)
• Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications
  Hillel Kugler (Microsoft Research, Cambridge) and Itai Segall (Weizmann Institute of Science)
• Computing Weakest Strategies for Safety Games of Imperfect Information
  Wouter Kuijper (University of Twente) and Jaco Pol (University of Twente)

 

19.00-21.00 Reception at the Castle Museum
View Map
(Coaches leave campus at 18.45)

 

 

TUESDAY

 

TUESDAY 9:00-10:00 Invited Speaker
Central Hall, Chair: Luca de Alfaro

Temporal Reasoning about Program Executions
Rajeev Alur (University of Pennsylvania)

 

10.00-10.30 Coffee (Exhibition Centre)

 

TUESDAY 10:30-12:30 (3 parallel 4-paper sessions)

CC - Register Allocation and Instruction Scheduling
Room P/L002, Chair: Peter Thiemann

• SSA Elimination after Register Allocation
  Fernando Pereira (UCLA) and Jens Palsberg (UCLA)
• Register Spilling and Live-Range Splitting for SSA-Form Programs
  Matthias Braun (Universität Karlsruhe) and Sebastian Hack (Saarland University)
• Enhanced Hierarchical Instruction Scheduling for Tiled Dataflow Architectures
  Muhammad Umar Farooq (University of Texas at Austin) and Lizy John (University of Texas at Austin)
• Scheduling Tasks to Maximize Usage of Aggregate Variables In Place
  Samah Abu-Mahmeed (Rice University), Zoran Budimlic (Rice University), Cheryl McCosh (Rice University), Ken Kennedy (Rice University), Kaushik Ravindran (National Instruments), Jacob Kornerup (National Instruments), Kevin Hogan (National Instruments) and Steve Rogers (National Instruments)

FOSSACS - Automata Theory
Room P/L001, Chair: Moshe Vardi

• Tighter Bounds for the Determinisation of Büchi Automata
  Sven Schewe (University of Liverpool)
• Lower Bounds on Witnesses for Nonemptiness of Universal co-Büchi Automata
  Orna Kupferman (Hebrew University) and Nir Piterman (Imperial College)
• Interrupt Timed Automata
  Beatrice Berard (LIP6, Université Pierre et Marie Curie) and Serge Haddad (LSV, ENS Cachan)
• Parameter Reduction in Grammar-Compressed Trees
  Markus Lohrey (University of Leipzig), Sebastian Maneth (NICTA and University of New South Wales) and Manfred Schmidt-Schauss (Inst. für Informatik, J.W. Goethe-University, Frankfurt)

TACAS - Verification of Concurrent Programs
Room P/X001, Chair: Natasha Sharygina

• Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads
  Mohamed Faouzi Atig (Liafa, CNRS and University Paris Diderot), Ahmed Bouajjani (Liafa, CNRS and University Paris Diderot) and Shaz Qadeer (Microsoft Research, Redmond)
• Semantic Reduction of Thread Interleavings for Concurrent Programs
  Vineet Kahlon (NEC Laboratories), Sriram Sankaranarayanan (NEC Laboratories) and Aarti Gupta (NEC Laboratories)
• Inferring Synchronization under Limited Observability
  Martin Vechev (IBM Research), Eran Yahav (IBM Research) and Greta Yorsh (IBM Research)
• The Complexity of Predicting Atomicity Violations
  Azadeh Farzan (University of Toronto) and Parthasarathy Madhusudan (University of Illinois at Urbana Champaign)

 

12.30-14.30 Lunch (Roger Kirk Centre)

 

TUESDAY 14:30-16:30 (3 parallel 4-paper sessions)

 

CC - Specialisation
Room P/L002, Chair: Silvia Breu

• Dynamic Look Ahead Compilation
  Simone Campanoni (Politecnico di Milano), Martino Sykora (Politecnico di Milano), Giovanni Agosta (Politecnico di Milano) and Stefano Crespi Reghizzi (DEI - Politecnico di Milano)
• Precise Management of Scratchpad Memories for Localising Array Accesses in Scientific Codes
  Armin Gröβlinger (University of Passau)
• Blind Optimizations for Exploiting Hardware Features
  Dan Knights (University of Colorado), Todd Mytkowicz (University of Colorado), Peter Sweeney (IBM), Michael Mozer (University of Colorado) and Amer diwan (UNiversity of Colorado)
• How to CPS Transform a Monad
  Annette Bieniusa (Universität Freiburg) and Peter Thiemann (Universität Freiburg)

FOSSACS - Processes and Models
Room P/L001, Chair: Luis Caires

• The Calculus of Handshake Configurations
  Luca Fossati (University Paris 7 - PPS) and Daniele Varacca (PPS - CNRS and University Paris 7)
• On the Expressive Power of Restriction and Priorities in CCS with Replication
  Jesus Aranda (LIX, Ecole Polytechnique), Frank Valencia (LIX, Ecole Polytechnique) and Cristian Versari (University of Bologna)
• Normal Bisimulations in Calculi with Passivation
  Sergueï Lenglet (UJF Grenoble), Alan Schmitt (INRIA) and Jean-Bernard Stefani (INRIA)
• Reactive Systems, Barbed Semantics, and the Mobile Ambients
  Filippo Bonchi (University of Pisa), Fabio Gadducci (University of Pisa) and Giacoma Monreale

TACAS - Tools II
Room P/X001, Chair: Panagiotis Manolios

• MoonWalker: Verification of .NET Programs
  Niels Aan de Brugh (OCÉ Venlo), Viet Yen Nguyen (RWTH Aachen) and Theo Ruys (University of Twente)
• Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays
  Robert Brummayer (Johannes Kepler University, Linz) and Armin Biere (Johannes Kepler University, Linz)
• The YOGI Project: Software Property Checking via Static Analysis and Testing
  Aditya Nori (Microsoft Research, India), Sriram Rajamani (Microsoft Research, India), Saideep Tetali (Microsoft Research, India) and Aditya Thakur (University of Wisconsin-Madison)
• TaPAS: The Talence Presburger Arithmetic Suite
  Jérôme Leroux (LaBRI, CNRS) and Gérald Point (LaBRI, CNRS)

 

16.30-17.00 Coffee (Exhibition Centre)

 

TUESDAY 17:00-18:30 (2 parallel 3-paper sessions)

FOSSACS - Security
Room P/L001, Chair: Catuscia Palamidessi

• On the Foundations of Quantitative Information Flow
  Geoffrey Smith (Florida International University)
• Cryptographic Protocol Composition via the Authentication Tests
  Joshua Guttman (MITRE Corporation)
• Bisimulation for Demonic Schedulers
  Konstantinos Chatzikokolakis (Eindhoven University of Technology), Gethin Norman (Oxford University) and David Parker (Oxford University)

TACAS - Model Checking II
Room P/X001, Chair: Rajeev Alur

• Transition-based Directed Model Checking
  Martin Wehrle (University of Freiburg), Sebastian Kupferschmid (University of Freiburg) and Andreas Podelski (University of Freiburg)
• Memorised Garbage Collection for Software Model Checking
  Viet Yen Nguyen (RWTH Aachen) and Theo Ruys (University of Twente)
• Hierarchical Adaptive State Space Caching based on Level Sampling
  Radu Mateescu (INRIA/VASY) and Anton Wijs (INRIA/VASY)

19.00-22.00 ETAPS Steering Committee Meeting (Room P/L005)

 

WEDNESDAY

 

WEDNESDAY 9:00-10:00 Invited Speaker (Unifying)
Central Hall, Chair: Gerald Lüttgen

 

Aspects of Synthesis

Wolfgang Thomas (RWTH Aachen)

 

10.00-10.30 Coffee (Exhibition Centre)

 

WEDNESDAY 10:30-12:30 (4 parallel 4-paper sessions)

 

ESOP - Typed Functional Programming
Room P/X001, Chair: Peter Thiemann

• Well-Typed Programs can't be Blamed
  Philip Wadler (University of Edinburgh) and Robert Findler (University of Chicago)
• Exploring the Design Space of Casts for Gradual Typing
  Jeremy Siek (University of Colorado at Boulder), Ronald Garcia (Indiana University) and Walid Taha (Rice University)
• Practical Variable-Arity Polymorphism
  T. Stephen Strickland (Northeastern University), Sam Tobin-Hochstadt (Northeastern University) and Matthias Felleisen (Northeastern University)
• Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming
  Matthew R. Lakin (University of Cambridge) and Andrew Pitts (University of Cambridge)

FASE - Model-Driven Development
Room P/L001, Chair: Daniel Varro

• Rewriting Logic Semantics and Verification of Model Transformations
  Artur Boronat (University of Leicester), Reiko Heckel (University of Leicester) and Jose Meseguer (University of Illinois at Urbana-Champaign)
• Confluence in Domain-Independent Product Line Transformations
  Jon Oldevik (University of Oslo, SINTEF ICT), Oystein Haugen (University of Oslo, SINTEF ICT) and Birger Mller-Pedersen (University of Oslo)
• Object Flow Validation for Refined Activity Diagrams
  Gabriele Taentzer (Philipps University of Marburg), Stefan Jurack (Philipps University of Marburg), Leen Lambers (TU Berlin), Katharina Mehner (Siemens AG) and Gerd Wierse (Philipps University of Marburg)
• A Category-Theoretical Approach to the Formalisation of Version Control in MDE
  Adrian Rutle (Bergen University College), Alessandro Rossini (University of Bergen), Yngve Lamo (Bergen University College) and Uwe Wolter (University of Bergen)

FASE - Synthesis and Adaptation
Room P/L002, Chair: Tiziana Margaria

• Controller Synthesis from LSC Requirements
  Hillel Kugler (Microsoft Research), Cory Plock (Microsoft Research) and Amir Pnueli (New York University)
• Interface Generation and Compositional Verification in JavaPathFinder
  Dimitra Giannakopoulou (CMU/NASA Ames Research Center) and Corina Pasareanu (CMU/ NASA Ames Research Center)
• A Formal Way from Text to Code Templates
  Guido Wachsmuth (Humboldt-Universität zu Berlin)
• Context-Aware Adaptive Services: The PLASTIC Approach
  Marco Autili (Università dell'Aquila), Paolo Di Benedetto (Università dell'Aquila) and Paola Inverardi (Università dell'Aquila)

FOSSACS - Probabilistic and Quantitative Models
Central Hall, Chair: Anna Philippou

• On Omega-Languages Defined by Mean-Payoff Conditions
  Gera Weiss (University of Pennsylvania), Aldric Degorre (Verimag), Rajeev Alur (University of Pennsylvania) and Oded Maler (Vérimag)
• Minimal Cost Reachability/Coverability in Priced Timed Petri Nets
  Richard Mayr (University of Edinburgh) and Parosh Abdulla (Uppsala University)
• Delayed Nondeterminism in Continuous-Time Markov Decision Processes
  Martin R. Neuhäuβer (RWTH Aachen), Marielle Stoelinga (University of Twente) and Joost-Pieter Katoen (RWTH Aachen)
• Concurrency, Sigma-Algebras and Probabilistic Fairness
  Samy Abbes (University Paris 7) and Albert Benveniste (IRISA)

 

12.39-1300 EASST General Assembly (Room P/L002)

12.30-14.30 Lunch (Roger Kirk Centre)

 

WEDNESDAY 14:30-15:30 Invited Speaker (Unifying)
Central Hall, Chair: Vladimiro Sassone

Using Category Theory to Design Programming Languages
John Reynolds (Carnegie Mellon University)

 

WEDNESDAY 15:30-16:30 (4 parallel 2-paper sessions)

ESOP - Computational Effects
Room P/X001, Chair: Eugenio Moggi

• Modular Monad Transformers
  Mauro Jaskelioff (University of Nottingham)
• Handlers of Algebraic Effects
  Gordon Plotkin (University of Edinburgh) and Matija Pretnar (University of Edinburgh)

FASE - Modeling
Room P/L002, Chair: Peter Olveczky

• Synchronous Modeling and Validation of Priority Inheritance Schedulers
  Erwan Jahier (CNRS/VERIMAG), Nicolas Halbwachs (CNRS/VERIMAG) and Pascal Raymond (CNRS/VERIMAG)
• Describing and Analyzing Behaviours over Tabular Specifications using (Dyn)Alloy
  Nazareno Aguirre (Universidad Nacional de Rio Cuarto), Marcelo Frias (FCEyN, Universidad de Buenos Aires), Mariano Moscato (FCEyN, Universidad de Buenos Aires), Tom Maibaum (McMaster University) and Alan Wassyng (McMaster University)

FOSSACS - Synthesis
Room P/L001, Chair: Luca de Alfaro

• Synthesis from Component Libraries
  Yoad Lustig (Rice University) and Moshe Y. Vardi (Rice University)
• Realizability of Concurrent Recursive Programs
  Benedikt Bollig (LSV, ENS Cachan, CNRS), Manuela-Lidia Grindei (LSV, ENS Cachan, CNRS) and Peter Habermehl (LIAFA University Paris 7)

TACAS - Parametric Analysis
Central Hall, Chair: Parosh Abdullah

• Static Analysis Techniques for Parameterised Boolean Equation Systems
  Simona Orzan (Eindhoven University of Technology), Wieger Wesselink (Eindhoven University of Technology) and Tim Willemse (Eindhoven University of Technology)
• Parametric Trace Slicing and Monitoring
  Feng Chen (University of Illinois at Urbana-Champaign) and Grigore Ro¸su (University of Illinois at Urbana-Champaign)

 

16.30-17.00 Coffee (Exhibition Centre)

 

WEDNESDAY 17:00-18:30 (4 parallel 3-paper sessions)

ESOP - Types for Object-Oriented Languages
Room P/X001, Chair: Jan Vitek

• Is Structural Subtyping Useful? An Empirical Study
  Donna Malayeri (Carnegie Mellon University) and Jonathan Aldrich (Carnegie Mellon University)
• An Interval-based Inference of Variant Parametric Types
  Florin Craciun (Durham University), Wei-Ngan Chin (Durham University), Guanhua He (Durham University) and Shengchao Qin (Durham University)
• Existential Quantification for Variant Ownership
  Nicholas Cameron (Imperial College London) and Sophia Drossopoulou (Imperial College London)

FASE - Testing and Debugging
Room P/L002, Chair: Dimitra Giannakopoulou

• Reducing the Costs of Bounded-Exhaustive Testing
  Vilas Jagannath (University of Illinois at Urbana-Champaign), Yun Young Lee (University of Illinois at Urbana-Champaign), Brett Daniel (University of Illinois at Urbana- Champaign) and Darko Marinov (University of Illinois at Urbana-Champaign)
• Logical Testing: Hoare-style Specification Meets Executable Validation
  Kathryn E Gray (University of Cambridge) and Alan Mycroft (University of Cambridge)
• Cross-Entropy-Based Replay of Concurrent Programs
  Hana Chockler (IBM Research), Eitan Farchi (IBM Research), Benny Godlin (IBM Research) and Sergey Novikov (Weizmann Institute)

FOSSACS - Program Analysis and Semantics
Room P/L001, Chair: Barbara Konig

• Beyond Shapes: Lists with Ordered Data
  Etienne Lozes (LSV, ENS Cachan, CNRS), Remi Brochenin (CNRS) and Kshitij Bansal (Chennai Mathematical Institute)
• Interprocedural Dataflow Analysis over Weight Domains with Infinite Descending
  Chains Morten Kühnrich (Aalborg University), Stefan Schwoon (Technische Universität München), Jiri Srba (Aalborg University) and Stefan Kiefer (Technische Universität München)
• Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
  Lars Birkedal (IT University of Copenhagen), Kristian Støvring (IT University of Copenhagen) and Jacob Thamsborg (IT University of Copenhagen)

TACAS - Generative Approaches
Central Hall, Chair: Gerald Lüttgen

• From Tests to Proofs
  Ashutosh Gupta (MPI-SWS), Rupak Majumdar (University of California, Los Angeles) and Andrei Rybalchenko (MPI-SWS)
• Test Input Generation for Programs with Pointers
  Dries Vanoverberghe (Katholieke Universiteit Leuven), Nikolai Tillmann (Microsoft Research, Redmond) and Frank Piessens (Katholieke Universiteit Leuven)
• Specification Mining With Few False Positives
  Claire Le Goues (University of Virginia) and Westley Weimer (University of Virginia)

 

19.30-23.00 Banquet at the National Railway Museum
View Map
(Coaches leave campus at 19.00)

 

 

THURSDAY

 

 

THURSDAY 9:00-10:00 Invited Speaker
Central Hall, Chair: Anna Philippou

Bridging the Gap Between Model-Based Development and Model Checking
Steven Miller (Rockwell Collins)

 

10.00-10.30 Coffee (Exhibition Centre)

 

THURSDAY 10:30-12:30 (3 parallel 4-paper sessions)

ESOP - Verification
Room P/L001, Chair: Xavier Leroy

• Formalising and Verifying Reference Attribute Grammars in Coq
  Max Schaefer (University of Oxford), Torbjörn Ekman (University of Oxford) and Oege de Moor (University of Oxford)
• Verified, Executable Parsing
  Aditi Barthwal (Australian National University) and Michael Norrish (NICTA)
• An Efficient Algorithm for Solving the Dyck-CFL-Reachability Problem on Trees
  Hao Yuan (Purdue University) and Patrick Eugster (Purdue University)
• Amortised Memory Analysis using the Depth of Data Structures
  Brian Campbell (University of Edinburgh)

FASE - Model Analysis
Room P/L002, Chair: Tom Maibaum

• Control Dependence for Extended Finite State Machines
  Kelly Androutsopoulos (King's College London), David Clark (King's College London), Mark Harman (King's College London), Zheng Li (King's College London) and Laurence Tratt (Bournemouth University)
• Proving Consistency of Pure Methods and Model Fields
  Rustan Leino (Microsoft Research) and Ronald Middelkoop (Technische Universiteit Eindhoven)
• On the Implementation of @pre
  Piotr Kosiuczenko (Institute of Information Systems, WAT, Warsaw)
• Formal Specification and Analysis of Timing Properties in Software Systems
  Musab AlTurki (University of Illinois at Urbana-Champaign), Dinakar Dhurjati (DOCOMO Communication Laboratories, USA), Dachuan Yu (DOCOMO Communication Laboratories, USA), Ajay Chander (DOCOMO Communication Laboratories, USA) and Hiroshi Inamura (DOCOMO Communication Laboratories, USA

TACAS - P rogram Analysis
Room P/X001, Chair: Nicolas Halbwachs

• Path Feasibility Analysis for String-Manipulating Programs
  Nikolaj Bjørner (Microsoft Research), Nikolai Tillmann (Microsoft Researc h) and Andrei Voronkov (University of Manchester)
• Symbolic String Veri^Lcation: Combining String Analysis and Size Analysi s
  Fang Yu (University of California, Santa Barbara), Tevfik Bultan (University of California, Santa Barbara) and Oscar Ibarra (University of California, Santa Barbara)
• Iterating Octagons
  Marius Bozga (Verimag/CNRS), Godrut¸a Gîrlea (Verimag/CNRS) and Radu Iosif (Verimag/CNRS)
• Verifying Reference Counting Implementation
  Michael Emmi (University of California, Los Angeles), Ranjit Jhala (University of California, San Diego), Eddie Kohler (University of California, Los Angeles) and Rupak Majumdar (University of California, Los Angeles)

 

12.30-14.30 Lunch (Roger Kirk Centre)

 

THURSDAY 14:30-15:30 Invited Speaker
Central Hall, Chair: Giuseppe Castagna

 

The Financial Crisis, a Lack of Contract Specification Tools: What can Finance Learn from Programming Language Design?
Jean-Marc Eber (LexiFi)

 

THURSDAY 15:30-16:30 (4 parallel 2-paper sessions)

ESOP - Security (Chair: Torben Amtoft)
Room P/L001, Chair: Torben Amtoft

• All Secrets Great and Small
  Delphine Demange (Université Rennes 1) and David Sands (Chalmers University)
• Type-Based Automated Verification of Authenticity in Cryptographic Protocols
  Daisuke Kikuchi (Tohoku University) and Naoki Kobayashi (Tohoku University)

FASE - Patterns
Room P/L002, Chair: Gabriele Taentzer

• Formal Foundation for Pattern-Based Modelling
  Paolo Bottoni (University of Rome), Esther Guerra (Universidad Carlos III de Madrid) and Juan de Lara (Universidad Autónoma de Madrid)
• Problem Oriented Documentation of Design Patterns
  Alexander Fülleborn (University Duisburg-Essen), Klaus Meffert (Technical University Ilmenau) and Maritta Heisel (University Duisburg-Essen)

TACAS - Hybrid Systems
Room P/X001, Chair: Stefan Kowalewski

• Falsification of LTL Safety Properties in Hybrid Systems
  Erion Plaku (Rice University), Lydia Kavraki (Rice University) and Moshe Vardi (Rice University)
• Computing Optimized Representations for Non-Convex Polyhedra by Detection and Removal of Redundant Linear Constraints
  Christoph Scholl (Albert-Ludwigs-Universität Freiburg), Stefan Disch (Albert-Ludwigs- Universität Freiburg), Florian Pigorsch (Albert-Ludwigs-Universität Freiburg) and Stefan Kupferschmid (Albert-Ludwigs-Universität Freiburg)

 

16.30-17.00 Coffee (Exhibition Centre)

 

THURSDAY 17:00-18:30 (3 parallel 3-paper sessions)

ESOP - Concurrency
Room P/L001, Chair: Peter Sewell

• A Theory of Non-Monotone Memory (Or: Contexts for Free)
  Eijiro Sumii (Tohoku University)
• Abstraction for Concurrent Objects
  Ivana Mijajlovic (Queen Mary, University of London), Peter O'Hearn (Queen Mary, University of London), Noam Rinetzky (Queen Mary, University of London) and Hongseok Yang (Queen Mary, University of London)
• A Minimization Algorithm for Symbolic Bisimilarity
  Filippo Bonchi (Università di Pisa) and Ugo Montanari (Università di Pisa)

FASE - Security
Room P/L002, Chair: Reiko Heckel

• Certification of Smart-Card Applications in Common Criteria: Proving Representation
  Correspondences Iman Narasamdya (Verimag) and Michael Perin (Université de Grenoble)
• Transformation of Type Graphs with Inheritance for Ensuring Security in E-Government
  Networks Frank Hermann (TU Berlin), Hartmut Ehrig (TU Berlin) and Claudia Ermel (TU Berlin)
• A Formal Connection between Security Automata and JML Annotations
  Marieke Huisman (University of Twente) and Alejandro Tamalet (Radboud University Nijmegen)

TACAS - Decision Procedures and Theorem Proving
Room P/X001, Chair: Alessandro Cimatti

• All-Termination(T)
  Panagiotis Manolios (Northeastern University) and Aaron Turon (Northeastern University)
• Ground Interpolation for the Theory of Equality
  Alexander Fuchs (University of Iowa), Amit Goel (Intel Corporation), Jim Grundy (Intel Corporation), Sava Krstic (Intel Corporation) and Cesare Tinelli (University of Iowa)
• Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
  Enrica Nicolini (LORIA & INRIA Nancy Grand Est), Christophe Ringeissen (LORIA & INRIA Nancy Grand Est) and Michaël Rusinowitch (LORIA & INRIA Nancy Grand Est)

 

FRIDAY

 

FRIDAY 9:00-10:00 Invited Speaker
Central Hall, Chair: Reiko Heckel

Scalable Analysis of Scalable Systems
Stephen Gilmore (Edinburgh University)

 

10.00-10.30 Coffee (Exhibition Centre)

 

FRIDAY 10:30-12:30 (2 parallel 4-paper sessions)

ESOP - Service-Oriented Computing
Room P/L001, Chair: Mariangiola Dezani-Ciancaglini

• Conversation Types
  Luís Caires (Universidade Nova de Lisboa) and Hugo Vieira (Universidade Nova de Lisboa)
• Abstract Processes in Orchestration Languages
  Maria Grazia Buscemi (IMT Lucca Institute for Advanced Studies) and Hernan Melgratti (University of Buenos Aires)
• Global Principal Typing in Partially Commutative Asynchronous Sessions
  Kohei Honda (Queen Mary, University of London), Dimitris Mostrous (Imperial College London) and Nobuko Yoshida (Imperial College London)
• Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Service
  Hridesh Rajan (Iowa State University), Jia Tao (Iowa State University), Steve Shaner (Iowa State University) and Gary T. Leavens (University of Central Florida)

FASE - Queries and Error Handling
Room P/L002, Chair: Martin Wirsing

• Automatic Failure Causal Path Computation Algorithms
  William Sumner (Purdue University) and Xiangyu Zhang (Purdue University)
• Mining API Error-Handling Specifications from Source Code
  Mithun Acharya (North Carolina State University) and Tao Xie (North Carolina State University)
• SNIFF: A Search Engine for Java using Free-Form Queries
  Shaunak Chatterjee (University of California, Berkeley), Sudeep Juvekar (University of California, Berkeley) and Koushik Sen (University of California, Berkeley)
• Inquiry and Introspection for Non-Deterministic Queries in Mobile Networks
  Vasanth Rajamani (University of Texas at Austin), Christine Julien (University of Texas at Austin), Jamie Payton (University of North Carolina at Charlotte) and Catalin Roman (Washington University in St. Louis)

 

12.30-14.30 Lunch (Roger Kirk Centre)

 

FRIDAY 14:30-16:30 (2 parallel 4-paper sessions)

 

ESOP - Parallel and Concurrent Programming
Room P/L001, Chair: Kostis Sagonas

• Automatic Parallelization with Separation Logic
  Mohammad Raza (Imperial College London), Cristiano Calcagno (Imperial College London) and Philippa Gardner (Imperial College London)
• Deny-Guarantee Reasoning
  Mike Dodds (University of Cambridge), Xinyu Feng (Toyota Technological Institute at Chicago), Matthew Parkinson (University of Cambridge) and Viktor Vafeiadis (Microsoft Research, Cambridge)
• A Basis for Verifying Multi-Threaded Programs
  Rustan Leino (Microsoft Research) and Peter Müller (ETH Zurich)
• SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs
  Caitlin Sadowski (University of California at Santa Cruz), Stephen Freund (Williams College) and Cormac Flanagan (University of California at Santa Cruz)

FASE - Tools (Demos) and Program Analysis
Room P/L002, Chair: Gerald Lüttgen

• HOL-TestGen - An Interactive Test-case Generation Framework
  Achim D. Brucker (SAP Research) and Burkhart Wolff (Universite Paris/Orsay)
• CADS*: Computer-Aided Development of Self-* Systems
  Radu Calinescu (University of Oxford) and Marta Kwiatkowska (University of Oxford)
• HAVE: Integrated Dynamic and Static Analysis for Atomicity Violations
  Qichang Chen (University of Wyoming), Liqiang Wang (University of Wyoming), Zijiang Yang (Western Michigan University) and Scott Stoller (Stony Brook University)
• Accurate and Efficient Structural Characteristic Feature Extraction Method for Clone Detection
  Hoan Nguyen (Iowa State University), Tung Nguyen (Iowa State University), Nam Pham (Iowa State University), Jafar Al-Kofahi (Iowa State University) and Tien Nguyen (Iowa State University)

 

16.30-17.00 Coffee (Exhibition Centre)

 

FRIDAY 17:00-18:00 (1 2-paper session)

FASE - Program Analysis
Room P/L002, Chair: Richard Paige

• Enhanced Property Specification and Verification in BLAST
  Ondrej Sery (Charles University of Prague)
• Finding Loop Invariants for Programs Over Arrays Using a Theorem Prover
  Laura Kovacs (EPFL Lausanne) and Andrei Voronkov (University of Manchester)

 

MAIN CONFERENCES' CLOSE