Programme of Tuesday,March 30

9.00
10.00
FASE Invited Talk
Gruia-Catalin Roman(Washington University, USA)
A Formal Treatment of Context-Awareness
Session chair: Tiziana Margaria and Michel Wermelinger
10.00
10.30
Coffee
10.30
12.30
ESOP
Spatial Logics

Session chair: 
Joshua Guttman

Compositional Analysis of Authentication Protocols
Michele Bugliesi, Riccardo Focardi, and  Matteo Maffei (Università Ca' Foscari di Venezia, I)

A Distributed Abstract Machine for Boxed Ambient Calculi
Andrew Phillips, Nobuko Yoshida, and Susan Eisenbach (Imperial College, UK)

A Dependently Typed Ambient Calculus
Cedric Lhoussaine and Vladimiro Sassone (University of Sussex, UK)

A Control Flow Analysis for Safe and Boxed Ambients
Francesca Levi (Università di Genova, I), Chiara Bodei (Università di Pisa, I)
FASE
Security and Web Services

Session chair: 
Reiko Heckel

Actor-Centric Modeling of User Rights   
Ruth Breu (Universität Innsbruck, A), Gerhard Popp (Technische Universität München, D)

Modeling Role-Based Access Control Using Parameterized UML Models   
Dae-Kyoo Kim, Indrakshi Ray, Robert France, Na Li (Colorado State University, USA)

Compositional Nested Long Running Transactions   
Laura Bocchi (University of Bologna, I)

DaGen: A Tool for Automatic Translation from DAML-S to High-level Petri Nets
Daniel Moldt, Jan Ortmann (University of Hamburg, D)
TACAS
Tools

Session chair:  Bernhard Steffen


Vooduu: Verification of Object-Oriented Designs Using UPPAAL
Karsten Diethers, Michaela Huhn (Technische Universitaet Braunschweig, D)

CoPS - Checker of Persistent Security
Sabina Rossi (Università di Venezia, I), Carla Piazza, Enrico Pivato(Università di Udine, I)

Tampere Verification Tool
Henri Hansen, Heikki Virtanen, Henri Hansen, Antti Valmari, Juha Nieminen, Timo Erkkilä (Tampere University of Technology, SF)

SyncGen: An Aspect-Oriented Framework for Automatically Generating Synchronization Implementations from High-Level Specifications
John Hatcliff, Xianghua Deng, Matthew Dwyer, Masaaki Mizuno (Kansas State University, USA)

MetaGame: An Animation Tool for Model-Checking Games
Markus Müller-Olm, Haiseung Yoo (Universitaet Dortmund, D)

A Tool for Checking ANSI-C Programs
Daniel Kroening, Edmund Clarke (Carnegie Mellon University, USA), Flavio Lerda (NASA Ames Research Center, USA)
eTX
12.30
14.30
Lunch
14.30
16.30
ESOP
Distributed Programming

Session chair: 
Markus Müller-Olm

Linear Types for Packet Processing
Robert Ennals, Intel Research,Richard Sharp and Alan Mycroft  (Cambridge University, UK)

Modal Proofs As Distributed Programs
Limin Jia and David Walker (Princeton University, USA)

ULM, A Core Programming Model for Global Computing
Gerard Boudol (INRIA, Sophia Antipolis, F)

A Semantic Framework for Designer Transactions
Jan Vitek, Suresh Jagannathan, Adam Welc, Antony L. Hosking (Purdue University, USA)
FASE
Modeling and Requirements

Session chair:  Maura Cerioli

Integrating Meta Modelling Aspects with Graph Transformation for Efficient Visual Language Definition and Model Manipulation
Roswitha Bardohl, Hartmut Ehrig (Technische Universität Berlin, D), Juan de Lara (Universidad Autónoma de Madrid, E), Gabriele Taentzer (Technische Universität Berlin, D)

An Operational Semantics for Stateflow   
Grégoire Hamon, John Rushby (SRI International, USA)

Improving Use Case Based Requirements Using Formally Grounded Specifications
Christine Choppy (Université Paris XIII, F), Gianna Reggio (Università di Genova, I)

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, UK)
FOSSACS
Specification Formalisms

Session chair:  Parosh Abdula

Partial Correctness Assertions Provable in Dynamic Logics
Daniel Leivant (Indiana University, USA)

Choice in Dynamic Linking
Martin Abadi (University of California, USA),
Georges Gonthier (Microsoft Research, USA) and Benjamin Werner (INRIA, F) 

Specifying and Verifying Partial Order Properties using Template MSCs
Blaise  Genest (LIAFA, F), Marius Minea (Politehnica University of Timisoara, RO), Anca Muscholl (LIAFA, F)  and Doron Peled (University of Warwick, UK)

Reasoning about Dynamic Policies
Riccardo Pucella and Vicky Weissman (Cornell University, USA)
eTX
16:30
17.00
Coffee
17.00
18.30
ESOP
Logics and Typing

Session chair:  David Schmidt

Semantical Analysis of Specification Logic, An Operational Approach
Dan Ghica (Oxford University, UK)

Answer Type Polymorphism in Call-by-name Continuation Passing
Hayo Thielecke (University of Birmingham, UK)

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, UK), A. J. Kfoury (Boston University, USA)
FASE
Testing

Session chair:  Mauro Pezzè

Automated Debugging using Path-Based Weakest Preconditions
Haifeng He, Neelam Gupta (The University of Arizona, USA)

Filtering TOBIAS combinatorial test suites   
Yves Ledru, Lydie du Bousquet, Olivier Maury, Pierre Bontron (IMAG, F)

Systematic Testing of Software Architectures in the C2 style   
Henry Muccini (Università degli Studi dell'Aquila, I), Marcio Dias, D.J. Richardson (University of California at Irvine, USA)
TACAS
Explicite State/Petri Nets

Session chair:  Antti Valmari

Obtaining Memory-Efficient Reachability Graph Representations Using the Sweep-Line Method
Michael Westergaard, Thomas Mailund (University of Aarhus, DK)

Automated generation of a progress measure for the sweep-line method
Karsten Schmidt (Humboldt Universitaet Berlin, D)

Tarjan's Algorithm Makes On-the-fly LTL Verification More Efficient
Jaco Geldenhuys, Antti Valmari (Tampere University of Technology, SF)
eTX