\documentclass[english,a4paper,12pt]{article}
%\usepackage{b5}
\RequirePackage[a4paper,top=2.5cm,left=2cm,right=2cm,bottom=2.5cm]{geometry}
%\parindent 0pt
%\parskip 3pt
\usepackage{babel}
\usepackage[latin1]{inputenc}
%\usepackage[utf8]{inputenc}
%\usepackage{fancyvrb}
\usepackage{t1enc}
\usepackage{url}
\usepackage{aeguill}
\usepackage{graphicx}
\usepackage{pdfpages}
\begin{document}

%\title{Programa ETAPS}
%\author{Braga, 2007}
%\date{}

\includepdf[fitpaper=true]{capa.pdf}

\subsection*{Steering Committee}

      Perdita Stevens, Edinburgh (Chair)

      Luca Aceto, Aalborg and Reykjavík

      Rastislav Bodik, Berkeley

      Maura Cerioli, Genova

      Matt Dwyer, Lincoln

      Hartmut Ehrig, Berlin

      José Luiz Fiadeiro, Leicester

      Marie-Claude Gaudel, Paris

      Roberto Gorrieri, Bologna

      Reiko Heckel, Leicester

      Michael Huth, London

      Joost-Pieter Katoen, Aachen

      Paul Klint, Amsterdam

      Jens Knoop, Vienna

      Shriram Krishnamurthi , Brown

      Kim Larsen, Aalborg

      Tiziana Margaria, Potsdam

      Ugo Montanari, Pisa

      Rocco de Nicola, Firenze

      Hanne Riis Nielson, Copenhagen

      Jens Palsberg,Indiana

      Don Sannella, Edinburgh

      João Saraiva, Braga

      Vladimiro Sassone, Southampton

      Helmut Seidl , Munique

      Peter Sestoft, Copenhagen

      Andreas Zeller, Saarbrücken

      Lenore Zuck, Chicago

\subsection*{Organizing Committee}

      João Alexandre Saraiva (Chair)

      Joost Visser (Satellite events)

      Luis Soares Barbosa (Satellite events)

      José Nuno Oliveira

      Pedro Rangel Henriques

      José João Almeida

      António Nestor Ribeiro

      Jorge Sousa Pinto

      José Bacelar Almeida (Website)

      Victor Francisco Fonte (Website)

\newpage

\tableofcontents
\newpage

\section*{Welcome}

\subsection*{Welcome to Braga}

Braga, capital of the Minho province, is an ancient city in the heart of
the green and fertile region known as the Costa Verde. The region is known
for its attractiveness in terms of climate, gastronomy, prices, and
culture. The region is served by the Oporto international airport,
providing direct flights to many major European cities.
Braga is known for its barroque churches and splendid 18th century houses.
The old city is solemn and antique, but animated with commercial activity
and academic life.


\subsection*{Welcome to ETAPS 2007}

\section{Etaps Locations}

\section{Main Conferences}
\begin{itemize}
\item \textbf{CC 2007}
, International Conference on Compiler Construction 
\item \textbf{ESOP 2007}
, European Symposium on Programming 
\item \textbf{FASE 2007}
, Fundamental Approaches to Software Engineering 
\item \textbf{FOSSACS 2007}
, Foundations of Software Science and Computation Structures 
\item \textbf{TACAS 2007}
, Tools and Algorithms for the Construction and Analysis of Systems 
 
\end{itemize}
\subsection{CC}
\subsubsection{International Conference on Compiler Construction}


  CC is interested in work on processing programs in the most general sense: analyzing, transforming or executing input that describes how a system operates, including traditional compiler construction as a special case. 


  Topics of interest include, but are not limited to: \begin{itemize}
\item \emph{compilation and interpretation techniques}
, including program representation and analysis, code generation and code optimization 
\item \emph{run-time techniques}
, including memory management and dynamic and just-in-time compilation 
\item \emph{programming tools}
, from refactoring editors to checkers to compilers to virtual machines to debuggers 
\item \emph{techniques for specific domains}
, such as secure, parallel, distributed, embedded or mobile environments 
\item \emph{design of novel language constructs}
 and their implementation 
 
\end{itemize}
 
\subsubsection*{Programme Committee}
\begin{itemize}
\item Eric Allen, Sun Microsystems, Inc. 
\item Emery Berger, University of Massachusetts Amherst 
\item Rastislav Bodik, University of California, Berkeley 
\item William Cook, University of Texas at Austin 
\item Chen Ding, University of Rochester 
\item Sabine Glesner, Technical University of Berlin 
\item Dan Grossman, University of Washington 
\item Rajiv Gupta, University of Arizona 
\item Andrew Kennedy, Microsoft Research Cambridge 
\item Shriram Krishnamurthi, Brown University (co-chair) 
\item Christian Lengauer, University of Passau 
\item Cristina Videira Lopes, University of California, Irvine 
\item Todd Millstein, University of California, Los Angeles 
\item Martin Odersky, Ecole Polytechnique F\'ed\'erale de Lausanne (co-chair) 
\item G. Ramalingam, IBM Research 
\item Vijay Saraswat, IBM TJ Watson Research Center 
\item Zhong Shao, Yale University 
\item Yannis Smaragdakis, Georgia Tech 
\item Gregor Snelting, University of Passau 
\item Joost Visser, Universidade do Minho 
\item Reinhard Wilhelm, Saarland University 
 
\end{itemize}
\subsubsection*{Invited Speaker}


 Don Batory, University of Texas at Austin
\subsubsection*{Conference Page}


 \url{http://cc2007.cs.brown.edu/}
\subsection{ESOP}
\subsubsection{European Symposium on Programming,}


  ESOP is an annual conference devoted to fundamental issues in the specification, analysis, and implementation of programming languages and systems. This includes: 
\begin{itemize}
\item Design of programming languages and calculi and their formal properties
\item Techniques, methods, and tools for their implementation
\item Exploitation of programming styles within different programming paradigms
\item Automatic and manual methods for generating and reasoning about programs
\item The design and invention of systems and tools to assist in exploitation of the languages
 
\end{itemize}


  Contributions bridging the gap between theory and practice are particularly welcome. Topics traditionally covered by ESOP include programming paradigms and their integration, semantics, calculi of computation, security and privacy, advanced type systems, program analysis, program transformation, and practical algorithms based on theoretical developments. 
\subsubsection*{Programme Committee}
\begin{itemize}
\item  Steve Brookes - CMU Pitsburgh, USA 
\item  Gerard Boudol - INRIA Sophia Antipolis, France 
\item  Giuseppe Castagna - ENS Paris, France 
\item  Patrick Cousot - ENS Paris, France 
\item  Mads Dam - KTH stocholm, Sweden 
\item  Pierpaolo Degano - U. Pisa, Italy 
\item  Rocco De Nicola (Chair) - U. Firenze, Italy 
\item  Sophia Drossopoulou - Imperial College, UK 
\item  Cedric Fournet - Microsoft Cambridge, UK 
\item  Stefania Gnesi - ISTI CNR, Italy 
\item  Joshua Guttman - MITRE, USA 
\item  Chris Hankin - Imperial College, UK 
\item  Matthew Hennessy - U. Sussex, UK 
\item  Alan Jeffrey - Bell Labs, USA 
\item  John Mitchell - Stanford U., USA 
\item  Fleming Nielson - IMM Copenhagen, DK 
\item  Catuscia Palamidessi - INRIA Paris, France 
\item  Benjamin Pierce - U. Pennsilvania, USA 
\item  Andrei Sabelfeld - Chalmers, Sweden 
\item  Don Sannella - U. Edinburgh, UK 
\item  Bernhard Steffen - U. Dortmund, Germany 
\item  Walid Taha - Rice U., USA 
\item  Jan Vitek - Purdue U., USA 
\item  Martin Wirsing - LMU Munich, Germany 
\item  Xavier Leroy - INRIA Paris, France 
\item  Gianluigi Zavattaro - U. Bologna, Italy 
 
\end{itemize}
\subsubsection*{Invited Speaker}


 Andrew Pitts - Cambridge University, UK
\subsubsection*{Conference Page}


  \url{http://rap.dsi.unifi.it/esop07/}
\subsection{FASE}
\subsubsection{Fundamental Approaches to Software Engineering}


  The information society is increasingly reliant on software at all levels. Hence, the ability to produce software of high quality at low cost is crucial to technological and social progress. An intrinsic characteristic of software that integrates with real-world processes is the need to evolve in order to adjust to new or changing requirements. Maintaining quality while embracing change is one of the main challenges of software engineering. \\ 
 Software engineers have at their disposal theories, languages, methods, and tools that derive from both the systematic research of the academic community and the experience of practitioners. It is one of the roles of software engineering as a scientific discipline to foster feedback between academia and industry by proposing new solutions and evaluating the effectiveness of those solutions in practical contexts. \\ 
 Submissions to FASE may address either novel proposed solutions or the evaluation of solutions, but they must clearly identify: the problem being solved, the proposed solution and its relationship to existing solutions, and, in the case of evaluations, the context in which the evaluation was conducted. Contributions that combine the development of conceptual and methodological advances with their formal foundations and tool support are particularly encouraged. \\ 
 A non-exclusive list of topics of interest is given below. \begin{itemize}
\item  Requirements engineering: capture, consistency, and change management of software requirements 
\item  Software architectures: description and analysis of the architecture of individual systems or classes of applications 
\item  Implementation concepts and technologies: distributed, mobile, and embedded applications, service-oriented architectures and Web Services 
\item  Software processes: support for iterative, agile, and open source development 
\item  Model-driven development: design and semantics of semi-formal visual languages, consistency and transformation of models 
\item  Software evolution: refactoring, reverse and re-engineering, configuration management and architectural change, or aspect-orientation 
\item  Software quality: validation and verification of software using theorem proving, testing, analysis, metrics or visualization techniques 
\item  Application of formal methods to software development 
 
\end{itemize}
 
\subsubsection*{Programme Committee}
\begin{itemize}
\item  Luciano Baresi, Politecnico di Milano 
\item  Yolande Berbers, Katholieke Universiteit Leuven 
\item  Carlos Canal, University of M\'alaga 
\item  Myra Cohen, University of Nebraska 
\item  Ivica Crnkovic, M\"alardalen University 
\item  Arie van Deursen, Delft University of Technology 
\item  Juergen Dingel, Queen's University 
\item  Matt Dwyer, University of Nebraska (co-chair) 
\item  Harald Gall, University of Zurich 
\item  Holger Giese, University of Paderborn 
\item  Martin Grosse-Rhode, Fraunhofer-ISST 
\item  Anthony Hall, independent consultant 
\item  Reiko Heckel, University of Leicester 
\item  Patrick Heymans, University of Namur 
\item  Paola Inverardi, University of L'Aquila 
\item  Valerie Issarny, INRIA-Rocquencourt 
\item  Natalia Juristo, Universidad Politecnica de Madrid 
\item  Kai Koskimies, Tampere University of Technology 
\item  Patricia Lago, Vrije Universiteit 
\item  Ant\'onia Lopes, University of Lisbon (co-chair) 
\item  Mieke Massink, CNR-Institute of Information Science and Technology 
\item  Carlo Montangero, University of Pisa 
\item  Barbara Paech, University of Heidelberg 
\item  Leila Ribeiro, Federal University of Rio Grande do Sul 
\item  Robby, Kansas State University 
\item  Catalin Roman, Washington University 
\item  Sebastian Uchitel, Imperial College London and University of Buenos Aires 
\item  Jianjun Zhao, Shanghai Jiao Tong University 
 
\end{itemize}
\subsubsection*{Invited Speaker}


 Jan Bosch (Nokia, Finland)
\subsubsection*{Conference Page}


 \url{http://fase07.di.fc.ul.pt}
\subsection{FOSSACS}
\subsubsection{Foundations of Software Science and Computation Structures}


  FOSSACS seeks original papers on foundational research with a clear significance for software science. The conference invites submissions on theories and methods to support the analysis, integration, synthesis, transformation, and verification of programs and software systems. 
 Topics covered include, but are not limited to: \begin{itemize}
\item  Algebraic models, 
\item  Automata and language theory, 
\item  Behavioural equivalences, 
\item  Categorical models, 
\item  Computation processes over discrete and continuous data, 
\item  Infinite state systems 
\item  Computation structures, 
\item  Logics of programs, 
\item  Modal, spatial, and temporal logics, 
\item  Models of concurrent, reactive, distributed, and mobile systems, 
\item  Process algebras and calculi, 
\item  Semantics of programming languages, 
\item  Software specification and refinement, 
\item  Type systems and type theory. 
\item  Fundamentals of security 
\item  Semi-structured data 
\item  Program correctness and verification 
 
\end{itemize}
\subsubsection*{Programme Committee}
\begin{itemize}
\item  Martin Abadi, University of California at Santa Cruz and Microsoft Research 
\item  Michael Benedikt, Bell Laboratories 
\item  Ahmed Bouajjani, Universit\'e Paris 7 
\item  Cristiano Calcagno, Imperial College London 
\item  Didier Caucal, IRISA-CNRS, Rennes 
\item  Flavio Corradini, Univerty of Camerino 
\item  Robert van Glabbeek, Stanford Universit 
\item  Andrew D. Gordon, Microsoft Research, Cambridge 
\item  Hendrik Jan Hoogeboom, Leiden University 
\item  Anna Ingolfsdottir, Aalborg University 
\item  Florent Jacquemard LSV, ENS de Cachan 
\item  Werner Kuich, TU Wien 
\item  Kamal Lodaya, Institute of Mathematical Sciences, Chennai 
\item  Antoine Min\'e, ENS Rue d'Ulm, Paris 
\item  Damian Niwinski, Warsaw University 
\item  David A. Schmitt, University of Kansas 
\item  Stefan Schwoon, Universit\"at Stuttgart 
\item  Helmut Seidl, TU M\"unchen (chair) 
\item  Scott A. Smolka, State University of New York at Stony Brook 
\item  P.S. Thiagarajan, National University of Singapore 
\item  Sophie Tison, Universit\'e des Sciences et Technologies de Lille 
\item  Heiko Vogler, TU Dresden 
\item  Christoph Weidenbach, Max-Planck-Institut f\"ur Informatik, Saarbr\"ucke 
 
\end{itemize}
\subsubsection*{Invited Speaker}


  Radha Jagadeesan, DePaul University 
\subsubsection*{Conference Page}


  \url{http://www2.in.tum.de/~seidl/fossacs07/}
\subsection{TACAS}
\subsubsection{Tools and Algorithms for the Construction and Analysis of Systems}


  TACAS is a forum for researchers, developers and users interested in rigorously based tools and algorithms for the construction and analysis of systems. The conference serves to bridge the gaps between different communities that share common interests in, and techniques for, tool development and its algorithmic foundations. The research areas covered by such communities include but are not limited to formal methods, software and hardware verification, static analysis, programming languages, software engineering, real-time systems, communications protocols, and biological systems. The TACAS forum provides a venue for such communities at which common problems, heuristics, algorithms, data structures and methodologies can be discussed and explored. In doing so, TACAS aims to support researchers in their quest to improve the utility, reliability, flexibility and efficiency of tools and algorithms for building systems. 
 Tool descriptions and case studies with a conceptual message, as well as theoretical papers with clear relevance for tool construction are all encouraged. The specific topics covered by the conference include, but are not limited to, the following: \begin{itemize}
\item  Specification and verification techniques for finite and infinite-state systems 
\item  Software and hardware verification 
\item  Theorem-proving and model-checking 
\item  System construction and transformation techniques 
\item  Static and run-time analysis 
\item  Abstraction techniques for modeling and validation 
\item  Compositional and refinement-based methodologies 
\item  Testing and test-case generation 
\item  Analytical techniques for secure, real-time, hybrid, critical, biological or dependable systems 
\item  Integration of formal methods and static analysis in high-level hardware design or software environments 
\item  Tool environments and tool architectures 
\item  SAT solvers 
\item  Applications and case studies 
 
\end{itemize}


  As TACAS addresses a heterogeneous audience, potential authors are strongly encouraged to write about their ideas and findings in general and jargon-independent, rather than in application- and domain-specific, terms. Authors reporting on tools or case studies are strongly encouraged to indicate how their experimental results can be reproduced and confirmed independently. 
\subsubsection*{Programme Committee}
\\ 


\begin{tabular}{c}


\begin{tabular}{l}
 Christel Baier \\ 
 Universit\"at Bonn, Bonn (Germany)  \\
 Armin Biere \\ 
 Johannes Kepler Universit\"at, Linz (Austria)  \\
 Jonathan Billington\\ 
 University of South Australia, Mawson Lakes (Australia)  \\
 Ed Brinksma \\ 
 ESI and University of Twente (The Netherlands)  \\
 Rance Cleaveland \\ 
 University of Maryland \& Fraunhofer USA Inc, College Park, Maryland (USA)  \\
 Byron Cook  (tool chair) \\ 
 Microsoft Research, Cambridge (UK)  \\
 Dennis Dams \\ 
 Lucent Technologies, Murray Hill, New Jersey (USA)  \\
 Marsha Chechik \\ 
 University of Toronto, Toronto (Canada)  \\
 Francois Fages \\ 
 INRIA Rocquencourt, Le Chesnay Cedex (France)  \\
 Kathi Fisler \\ 
 Worcester Polytechnic Institute, Worcester, Massachusetts (USA) 

\end{tabular}

 

\begin{tabular}{l}
 Limor Fix \\ 
 Intel Research Laboratory at Pittsburgh, Pittsburgh, Pennsylvania (USA)  \\
 Hubert Garavel \\ 
 INRIA Rhones-Alpes, Montbonnot Saint-Martin (France)  \\
 Susanne Graf \\ 
 VERIMAG, Grenoble - Gi\`eres (France)  \\
 Orna Grumberg  (co-chair)\\ 
 TECHNION - Israel Institute of Technology, Haifa (Israel)  \\
 John Hatcliff\\ 
 Kansas State University, Manhattan, Kansas (USA)  \\
 Holger Hermanns\\ 
 Universit\"at des Saarlandes, Saarbruecken (Germany)  \\
 Michael Huth (co-chair)\\ 
 Imperial College London, London (UK)  \\
 Daniel Jackson \\ 
 Massachusetts Institute of Technology, Cambridge, Massachusetts (USA)  \\
 Somesh Jha\\ 
 The University of Wisconsin at Madison, Madison, Wisconsin (USA) 

\end{tabular}

 

\begin{tabular}{l}
 Orna Kupferman \\ 
 Hebrew University, Jerusalem (Israel)  \\
 Marta Kwiatkowska \\ 
 University of Birmingham, Birmingham, England (UK)  \\
 Kim Larsen\\ 
 Aalborg University, Aalborg (Denmark)  \\
 Michael Leuschel\\ 
 Heinrich-Heine-Universit\"at D\"usseldorf, D\"usseldorf (Germany)  \\
 Andreas Podelski\\ 
 Max-Planck-Institut f\"ur Informatik, Saarbr\"ucken (Germany)  \\
 Tiziana Margaria-Steffen \\ 
 Universit\"at Potsdam, Potsdam (Germany)  \\
 Tom Melham \\ 
 Oxford University, Oxford (UK)  \\
 Natarajan Shankar\\ 
 SRI, Menlo Park, California (USA)  \\
 Bernhard Steffen\\ 
 Universit\"at Dortmund, Dortmund (Germany)  \\
 Lenore Zuck \\ 
 University of Illinois, Chicago, Illinois (USA) 

\end{tabular}

 

\end{tabular}

\subsubsection*{Invited Speaker}


  K. Rustan M. Leino (Microsoft Research, USA)
\subsubsection*{Conference Page}


  \url{http://www.doc.ic.ac.uk/tacas07/}


  
 \subsection{Programme of Main Conferences at ETAPS 2007}
\subsubsection{Programme of Monday, March 26}
\subsubsection*{09:00 - 10:30 SESSION 1 (Monday)}
\begin{description}
\item[Welcome ]\item[FOSSACS - Invited Talk (Chair: Helmut Seidl) ]\item Formal foundations for Aspects 
\item Radha Jagadeesan (DePaul University, USA) 

\end{description}
\subsubsection*{10:30 - 11:00 Coffee}
\subsubsection*{11:00 - 12:30 SESSION 2 (Monday)}
\begin{description}
\item[CC - Architecture (Chair: Martin Odersky) ]\item New Algorithms for SIMD Alignment 
\item Liza Fireman (Technion), Erez Petrank (Microsoft Research), Ayal Zaks (IBM Haifa Research Laboratory) 
\item Preprocessing Strategy for Effective Modulo Scheduling on Multi-Issue Digital Signal Processors 
\item Doosan Cho (Seoul National University), Ravi Ayyagari (Boise State University), Gang-Ryung Uh (Bosie State University), Yunheung Paek (Seoul National University) 
\item Compiler Directed Power Optimization for Partitioned Memory Architectures 
\item K. Shyam, R. Govindarajan (Indian Institute of Science) 
\item[FOSSACS - Games and Mu Calculus (Chair: Helmut Seidl) ]\item Optimal Strategy Synthesis in Stochastic M\"uller Games 
\item Krishnendu Chatterjee (Univ. of California, Berkeley) 
\item Generalized Parity Games 
\item Nir Piterman (EPFL Switzerland), Krishnendu Chatterjee (Univ. of Califonria, Berkeley), Thomas A. Henzinger (EPFL Switzerland) 
\item Enriched mu-Calculi Module Checking 
\item Aniello Murano (Univ. di Napoli), Alessandro Ferrante (Univ. di Salerno) 
\item[TACAS - Software Verification (Chair: Natasha Sharygina) ]\item Shape Analysis by Graph Decomposition 
\item Roman Manevich (Tel Aviv University), Joshua Berdine, Byron Cook (Microsoft Reasearch Cambridge), Ganesan Ramalingam (Microsoft Research India), and Mooly Sagiv (Tel Aviv University) 
\item A reachability predicate for analyzing low-level software 
\item Shaunak Chatterjee (Indian Institute of Technology at Kharagpur), Shuvendu K. Lahiri, Shaz Qadeer (Microsoft Research), and Zvonimir Rakamaric (University of British Columbia) 
\item Generating Representation Invariants of Structurally Complex Data 
\item Muhammad Zubair Malik, Aman Pervaiz, and Sarfraz Khurshid (University of Texas at Austin) 

\end{description}
\subsubsection*{12:30 - 14:30 Lunch}
\subsubsection*{14:30 - 16:30 SESSION 3 (Monday)}
\begin{description}
\item[CC - Garbage Collection and Program Analysis (Chair: Reinhard Wilhelm) ]\item Using Prefetching to Improve Reference-Counting Garbage Collectors 
\item Harel Paz (IBM Haifa Research Laboratory), Erez Petrank (Microsoft Research) 
\item Accurate Garbage Collection in Uncooperative Environments with Lazy Pointer Stacks 
\item Jason Baker, Antonio Cunei, Filip Pizlo, Jan Vitek (Purdue University) 
\item Correcting the Dynamic Call Graph Using Control-Flow Constraints 
\item Byeongcheol Lee, Kevin Resnick, Michael D. Bond, Kathryn S. McKinley (University of Texas at Austin) 
\item Obfuscating Java: the Most Pain for the Least Gain 
\item Michael Batchelder, Laurie Hendren (McGill University) 
\item[FOSSACS - Logic (Chair: Hubert Comon) ]\item The Complexity of Generalized Satisfiability for Linear Temporal Logic 
\item Thomas Schneider (Univ. Jena), Henning Schnoor (Univ. Hannover), Ilka Schnoor (Univ. Hannover), Michael Bauland (Univ. Hannover), Heribert Vollmer (Univ. Hannover) 
\item PDL with intersection and converse is 2EXP-complete 
\item Markus Lohrey (Univ. Stuttgart), Carsten Lutz (TU Dresden), Stefan G\"oller (Univ. Stuttgart) 
\item On the Expressiveness and Complexity of ATL 
\item Nicolas Markey (ENS Cachan), Ghassan Oreiby (ENS Cachan), Francois Laroussinie (ENS Cachan) 
\item Formalising the pi-calculus using Nominal Logic 
\item Jesper Bengtson (Uppsala Univ.), Joachim Parrow (Uppsala Univ.) 
\item[TACAS - Probabilistic Model Checking and Markov Chains (Chair: Holger Hermanns) ]\item Multi-Objective Model Checking of Markov Decision Processes 
\item Kousha Etessami (University of Edinburgh), Marta Kwiatkowska (Birmingham University), Moshe Y. Vardi (Rice University), and Mihalis Yannakakis (Columbia University) 
\item PReMo: an analyzer for Probabilistic Recursive Models 
\item Dominik Wojtczak and Kousha Etessami (University of Edinburgh) 
\item Counterexamples in Probabilistic Model Checking 
\item Tingting Han and Joost-Pieter Katoen (RWTH Aachen and University of Twente) 
\item Bisimulation minimisation mostly speeds up probabilistic model checking 
\item Joost-Pieter Katoen (RWTH Aachen and University of Twente), Tim Kemna (University of Twente), Ivan Zapreev (RWTH Aachen and University of Twente), and David N. Jansen (University of Twente) 

\end{description}
\subsubsection*{16:30 - 17:00 Coffee}
\subsubsection*{17:00 - 18:30 SESSION 4 (Monday)}
\begin{description}
\item[CC - Register Allocation (Chair: Ganesan Ramalingam) ]\item A Fast Cutting-Plane Algorithm for Optimal Coalescing 
\item Daniel Grund (Saarland University), Sebastian Hack (University of Karlsruhe) 
\item Register Allocation and Optimal Spill code Scheduling in Software Pipelined Loops using 0-1 Integer Linear Programming Formulation 
\item Santosh G. Nagarakatte, R. Govindarajan (Indian Institute of Science) 
\item Extended Linear Scan: an Alternate Foundation for Global Register Allocation 
\item Vivek Sarkar (IBM T.J. Watson Research Center), Rajkishore Barik (IBM India Research Laboratory) 
\item[FOSSACS - Formal Languages and Complexity (Chair: Igor Walukiewicz) ]\item Symbolic Reachability Analysis for Higher-Order Pushdown Systems 
\item Matthew Hague (Oxford Univ.), Luke Ong (Oxford Univ.) 
\item Complexity Results on Balanced Context-Free Languages 
\item Akihiko Tozawa (IBM Research, Tokyo), Yasuhiko Minamide (Univ. of Tsukuba) 
\item An Effective Algorithm for The Membership Problem for Extended Regular Expressions 
\item Grigore Rosu (Univ. of Illinois, Urbana) 
\item[TACAS - Static Analysis (Chair: Tiziana Margaria) ]\item Causal Concurrent Dataflow Analysis for Concurrent Programs 
\item Azadeh Farzan and P. Madhusudan (University of Illinois at Urbana-Champaign) 
\item Type-dependency Analysis and Program Transformation for Symbolic Execution 
\item Saswat Anand, Alessandro Orso, and Mary Jean Harrold (Georgia Institute of Technology) 
\item JPF--SE: A Symbolic Execution Extension to Java PathFinder 
\item Saswat Anand (Georgia Institute of Technology), Corina S. Pasareanu, and Willem Visser (NASA Ames Research Center) 

\end{description}
\subsubsection{Programme of Tuesday, March 27}
\subsubsection*{09:00 - 10:00 SESSION 1 (Tuesday)}
\begin{description}
\item[CC - Invited Talk (Chair: Shriram Krishnamurthi) ]\item On the Convergence of Program Refactoring, Program Synthesis, and Model Driven Development 
\item Don Batory (U. Austin, USA) 

\end{description}
\subsubsection*{10:00 - 10:30 Coffee}
\subsubsection*{10:30 - 12:30 SESSION 2 (Tuesday)}
\begin{description}
\item[CC - Program Analysis (Chair: Shriram Krishnamurthi) ]\item A Practical Escape and Effect Analysis for Building Lightweight Method Summaries 
\item Sigmund Cherem, Radu Rugina (Cornell University) 
\item Layout Transformations for Heap Objects Using Static Access Patterns 
\item Jinseong Jeon, Keoncheol Shin, Hwansoo Han (Korea Advanced Institute of Science and Technology) 
\item A New Elimination-Based Data Flow Analysis Framework 
\item Bernhard Scholz (University of Sydney), Johann Blieberger (Technische Universit$\backslash$''at Wien) 
\item A declarative framework for analysis and optimization components 
\item Henry Falconer, Paul H. J. Kelly, David M. Ingram, Michael R. Mellor, Tony Field, Olav Beckmann (Imperial College) 
\item[FOSSACS - Process Calculi (Chair: Pierpaolo Degano) ]\item A Distribution Law for CCS and a New Congruence Result for the Pi-calculus 
\item Daniel Hirschkoff (ENS Lyon), Damien Pous (ENS Lyon) 
\item Semantic barbs and biorthogonality 
\item Pawel Sobocinski (Univ. of Cambridge), Vladimiro Sassone (Univ. of Southampton), Julian Rathke (Univ. of Sussex) 
\item Logical Characterizations of Bisimulations for Discrete Probabilistic Systems 
\item Augusto Parma (Univ. di Verona), Roberto Segala (Univ. di Verona) 
\item Approximating a Behavioural Pseudometric without Discount for Probabilistic Systems 
\item Franck van Breugel (York Univ.), James Worrell (Oxford Univ.), Babita Sharma (York Univ.) 
\item[TACAS - Markov Chains and Real-Time Systems (Chair: Joost-Pieter Katoen) ]\item A Symbolic Algorithm for Optimal Markov Chain Lumping 
\item Salem Derisavi (Carleton University at Ottawa) 
\item Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations 
\item Lijun Zhang, Holger Hermanns (Saarland University), Friedrich Eisenbrand (University of Paderborn), and David N. Jansen(University of Twente) 
\item Model Checking Probabilistic Timed Automata with One or Two Clocks 
\item Marcin Jurdzinski (University of Warwick), Francois Laroussinie (ENS Cachan), and Jeremy Sproston (Universita di Torino) 
\item Adaptor synthesis for real-time components 
\item Massimo Tivoli (University of L'Aquila), Pascal Fradet, Alain Girault, Gregor Goessler (INRIA Rhone-Alpes) 

\end{description}
\subsubsection*{12:30 - 14:30 Lunch }
\subsubsection*{14:30 - 16:30 SESSION 3 (Tuesday)}
\begin{description}
\item[FOSSACS - Verification and Program Analysis (Chair: Cristiano Calcagno) ]\item Logical Reasoning for Higher-Order Functions with Local State 
\item Nobuko Yoshida (Imperial College London), Kohei Honda (Queen Mary), and Martin Berger (Imperial College London) 
\item Types and Effects for Resource Usage Analysis 
\item Massimo Bartoletti (Univ. di Pisa), Gian Luigi Ferrari (Univ. di Pisa), Pierpaolo Degano (Univ. di Pisa), Roberto Zunino (Univ. di Pisa) 
\item Relational Parametricity and Separation Logic 
\item Hongseok Yang (Univ. of London), Lars Birkedal (IT Univ. of Copenhagen) 
\item Polynomial Constraints for Sets with Cardinality Bounds 
\item Bruno Marnette (ENS Cachan), Martin Rinard (MIT, Cambridge, USA), Viktor Kuncak (MIT, Cambridge, USA) 
\item[TACAS (I) - Timed Automata and Duration Calculus (Chair: Joel Ouaknine) ]\item Deciding an Interval Logic with Accumulated Durations 
\item Martin Fraenzle (Universitat Oldenburg) and Michael R. Hansen (Technical University of Denmark) 
\item From Time Petri Nets to Timed Automata: an Untimed Approach 
\item Davide D'Aprile, Susanna Donatelli (Universita di Torino), Arnaud Sangnier (LSV-ENS Cachan), and Jeremy Sproston (Universita di Torino) 
\item Complexity in Simplicity: Flexible Agent-based State Space Exploration 
\item Jacob Illum Rasmussen, Gerd Behrmann, and Kim G. Larsen (Aalborg University) 
\item On Sampling Abstraction of Continuous Time Logic with Durations 
\item Paritosh K. Pandya (Tata Institute of Fundamental Research), Shankara Narayanan Krishna, and Kuntal Loya (Indian Institute of Technology at Bombay) 
\item[TACAS (II) - Assume-Guarantee Reasoning (Chair: Moshe Vardi) ]\item Assume Guarantee Synthesis 
\item Krishnendu Chatterjee (University of California, Berkeley) and Thomas A. Henzinger (EPFL) 
\item Optimized L* for Assume-Guarantee Reasoning 
\item Sagar Chaki (Software Engineering Institute) and Ofer Strichman (The Technion, Haifa) 
\item Refining Interface Alphabets for Compositional Verification 
\item Mihaela Gheorghiu (University of Toronto), Dimitra Giannakopoulou, and Corina S. Pasareanu NASA Ames Research Center) 
\item MAVEN: Modular Aspect Verification 
\item Max Goldman and Shmuel Katz (The Technion, Haifa) 

\end{description}
\subsubsection*{16:30 - 17:00 Coffee}
\subsubsection*{17:00 - 18:30 SESSION 4 (Tuesday)}
\begin{description}
\item[FASE - Evolution and Agents (Chair: Matt Dwyer) ]\item EQ-Mine: Predicting Short-Term Defects for Software Evolution 
\item Jacek Ratzinger (Vienna University of Technology, Austria), Martin Pinzger (University of Zurich, Switzerland), and Harald C. Gall (University of Zurich, Switzerland) 
\item An Approach to Software Evolution Based on Semantic Change 
\item Romain Robbes (University of Lugano, Switzerland), Michele Lanza (University of Lugano, Switzerland), and Mircea Lungu (University of Lugano, Switzerland) 
\item A Simulation-Oriented Formalization for a Psycholgical Theory 
\item Paulo Salem da Silva (University of S\~ao Paulo, Brazil), Ana C. V. de Melo (University of S\~ao Paulo, Brazil) 
\item[FOSSACS - Calculi (Chair: Antoine Mine) ]\item The Rewriting Calculus as a Combinatory Reduction System 
\item Clara Bertolissi (Univ. de Provence), Claude Kirchner (INRIA/LORIA, Nancy) 
\item Iterator Types 
\item Ian Mackie (King's College, London), Sandra Alves (Univ. of Porto), Maribel Fernandez (King's College, London), Mario Florido (Univ. of Porto) 
\item On the Stability by Union of Reducibiliy Candidates 
\item Colin Riba (INPL/LORIA, Nancy) 
\item[TACAS - Biological Systems (Chair: Radha Jagadeesan) ]\item Model Checking Liveness Properties of Genetic Regulatory Networks 
\item Gregory Batt and Calin Belta (Boston University), and Ron Weiss (Princeton University) 
\item Checking Pedigree Consistency with SAT 
\item Panagiotis Manolios, Marc Galceran Oms, and Sergi Oliva Valls (Georgia Institute of Technology, Atlanta) 
\item Don't Care Modeling: A logical framework for developing predictive system models 
\item Hillel Kugler (New York University), Amir Pnueli (New York University and the Weizmann Institute of Science), Michael Stern (Yale University), and E. Jane Albert Hubbard (New York University) 

\end{description}
\subsubsection{Programme of Wednesday, March 28}
\subsubsection*{09:00 - 10:10 SESSION 1 (Wednesday)}
\begin{description}
\item[Unifying Invited Talk (Chair: Perdita Stevens) ]\item There and Back Again: Lessons Learned on the Way to the Market 
\item Rance Cleaveland (University of Maryland/Fraunhofer USA Center for Experimental Software Engineering and Reactive Systems Inc., USA) 

\end{description}
\subsubsection*{10:10 - 10:30 Coffee}
\subsubsection*{10:30 - 12:30 SESSION 2 (Wednesday)}
\begin{description}
\item[ESOP - Models and Languages for Web Services (Chair: Matthew Hennessy) ]\item Structured Communication-Centred Programming for Web Services 
\item Marco Carbone (Imperial College London), Kohei Honda (Queen Mary, University of London) and Nobuko Yoshida (Imperial College London). 
\item CC-Pi: A Constraint-Based Language for Specifying Service Level Agreements 
\item Maria Grazia Buscemi (IMT Lucca ) and Ugo Montanari (University of Pisa). 
\item A Calculus for Orchestration of Web Services 
\item Alessandro Lapadula (University of Florence), Rosario Pugliese (University of Florence) and Francesco Tiezzi (University of Florence). 
\item A Concurrent Calculus with Atomic Transactions 
\item Lucia Acciai (Laboratoire d'Informatique Fondamentale, Marseille), Silvano Dal Zilio (Laboratoire d'Informatique Fondamentale, Marseille) and Michele Boreale (University of Florence). 
\item[FASE - Model Driven Development (Chair: Maura Cerioli) ]\item Integrating performance and reliability analysis in a Non-Functional MDA framework 
\item Vittorio Cortellessa (Universita degli Studi di L'Aquila, Italy) Antinisca Di Marco (Universita degli Studi di L'Aquila, Italy), and Paola Inverardi (Universita degli Studi di L'Aquila, Italy) 
\item Information Preserving Bidirectional Model Transformations 
\item Hartmut Ehrig (Technical University Berlin, Germany), Karsten Ehrig (University of Leicester, U.K.), Claudia Ermel (Technical University Berlin, Germany), Frank Hermann (Technical University Berlin, Germany), Gabriele Taentzer (Technical University Berlin, Germany) 
\item Activity-Driven Synthesis of State Machines 
\item Rolf Hennicker (Ludwig-Maximilians-Universitat Munchen,Germany), Alexander Knapp (Ludwig-Maximilians-Universitat Munchen, Germany) 
\item Flexible and Extensible Notations for Modeling 
\item Jimin Gao (University of Minnesota, USA), Mats Heimdahl (University of Minnesota, USA), Eric Van Wyk (University of Minnesota, USA) 
\item[FOSSACS - Automata (Chair: Markus Mueller-Olm) ]\item Tree Automata with Memory, Visibility and Structural Constraints 
\item Hubert Comon (ENS Cachan), Florent Jacquemard (INRIA/ENS Cachan), Nicolas Perrin (ENS Lyon) 
\item Model-Checking One-Clock Priced Timed Automata 
\item Patricia Bouyer (ENS Cachan), Nicolas Markey (ENS Cachan), Kim G. Larsen (Aalborg Univ.) 
\item Sampled Universality of Timed Automata 
\item Sampled Universality of Timed Automata, Pavel Krcal (Uppsala Univ.), Wang Yi (Uppsala Univ.), Parosh Abdulla (Uppsala Univ.) 
\item A Lower Bound on Web Services Composition 
\item Anca Muscholl (LABRI, Bordeaux), Igor Walukiewiczi (LABRI, Bordeaux) 
\item[FACAS - Abstraction Refinement (Chair: Shmuel Katz) ]\item Deciding Bit-Vector Arithmetic with Abstraction 
\item Randal E. Bryant (Carnegie Mellon University), Daniel Kroening (ETH Zuerich), Joel Ouaknine (Oxford University), Sanjit A. Seshia (University of California, Berkeley), Ofer Strichman (The Technion, Haifa), and Bryan Brady (University of California, Berkeley) 
\item Abstraction Refinement of Linear Programs with Arrays 
\item Alessandro Armando (Universita di Genova), Massimo Benerecetti (Universita di Napoli), and Jacopo Mantovani (Universita di Genova) 
\item Property-Driven Partitioning for Abstraction Refinement 
\item Roberto Sebastiani (Universita di Trento), Stefano Tonetta (University of Lugano), and Moshe Y. Vardi (Rice University) 
\item Combining Abstraction Refinement and SAT-based Model Checking 
\item Nina Amla and Kenneth McMillan (Cadence Design Systems) 

\end{description}
\subsubsection*{12:30 - 14:30 Lunch }
\subsubsection*{14:30 - 15:40 SESSION 3A (Wednesday)}
\begin{description}
\item[TACAS - Invited Talk (Chair: Rance Cleaveland) ]\item Verifying object-oriented software: lessons and challenges 
\item K. Rustan M. Leino (Microsoft Research, Redmond, USA) 

\end{description}
\subsubsection*{15:40 - 15:50 Break }
\subsubsection*{15:50 - 16:50 SESSION 3B (Wednesday)}
\begin{description}
\item[ESOP - Verification (Chair: Pierpaolo Degano) ]\item Modal I/O Automata for Interface and Product Line Theories 
\item Kim G. Larsen (Aalborg University), Ulrik Nyman (Aalborg University) and Andrzej Wasowski (IT University of Copenhagen) 
\item Using history invariants to verify observers 
\item Rustan Leino (Microsoft Research) and Wolfram Schulte (Microsoft Research) 
\item[ESOP - Term Rewriting (Chair: Don Sannella) ]\item On the implementation of construction functions for non-free concrete data types 
\item Frederic Blanqui (INRIA), Therese Hardin (Universite Paris 6) and Pierre Weis (INRIA) 
\item Anti-Pattern Matching 
\item Claude Kirchner (INRIA-LORIA Nancy), Radu Kopetz (INRIA-LORIA Nancy) and Pierre-Etienne Moreau (INRIA-LORIA Nancy) 
\item[FASE - Tool Demonstrations (Chair: Jos\'e Nuno Oliveira) ]\item Declared Type Generalization Checker: An Eclipse Plug-In for Programming with More General Types 
\item Markus Bach (University of Hagen, Germany) 
\item Florian Forster (University of Hagen, Germany) 
\item Friedrich Steimann (University of Hagen, Germany) 
\item S2A: A Compiler for Multi-Modal UML Sequence Diagrams 
\item David Harel (The Weizmann Institute of Science, Israel), Asaf Kleinbort (The Weizmann Institute of Science, Israel), Shahar Maoz (The Weizmann Institute of Science, Israel) 
\item[TACAS - Message Sequence Charts (Chair: Nina Amla) ]\item Detecting Races in Ensembles of Message Sequence Charts 
\item Edith Elkind (University of Liverpool), Blaise Genest (CNRS/IRISA), and Doron Peled (Bar Ilan University) 
\item Replaying Play in and Play out: Synthesis of Design Models from Scenarios by Learning 
\item Benedikt Bollig (LSV CNRS Cachan), Joost-Pieter Katoen, Carsten Kern (RWTH Aachen University), and Martin Leucker (TU Munich) 

\end{description}
\subsubsection*{16:50 - 17:15 Coffee}
\subsubsection*{17:15 - 18:45 SESSION 4 (Wednesday)}
\begin{description}
\item[ESOP - Language Based Security (Chair: Joshua Guttman) ]\item A Certified Lightweight Non-Interference Java Bytecode Verifier 
\item Gilles Barthe (INRIA Sophia Antipolis), David Pichardie (INRIA/IRISA) and Tamara Rezk (INRIA Sophia Antipolis) 
\item Controlling the What and Where of Declassification in Language-Based Security 
\item Heiko Mantel (RWTH Aachen University) and Alexander Reinhard (RWTH Aachen University) 
\item Cost Analysis of Java Bytecode 
\item Elvira Albert (Complutense University of Madrid), Puri Arenas (Complutense University of Madrid), Samir Genaim (Technical University of Madrid), German Puebla (Technical University of Madrid) and Damiano Zanardini (Technical University of Madrid) 
\item[ESOP - Logics and Correctness Proofs (Chair: Walid Taha) ]\item On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning 
\item Xinyu Feng (Yale University), Rodrigo Ferreira (Yale University) and Zhong Shao (Yale University) 
\item Abstract Predicates and Mutable ADTs in Hoare Type Theory 
\item Aleksandar Nanevski (Harvard University), Amal Ahmed (Toyota Technological Institute, Chicago), Greg Morrisett (Harvard University) and Lars Birkedal (IT University, Copenhagen) 
\item A Proof-producing Compiler for a Subset of Higher Order Logic 
\item Guodong Li (University of Utah) and Konrad Slind (University of Utah) 
\item[FASE - Distributed Systems (Chair: Holger Giese) ]\item Scenario-Driven Dynamic Analysis of Distributed Architectures 
\item George Edwards (University of Southern California, USA), Sam Malek (University of Southern California, USA), Nenad Medvidovic (University of Southern California, USA) 
\item Enforcing Architecture and Deployment Constraints of Distributed Component-based Software 
\item Chouki Tibermacine (University of South Brittany, France), Didier Hoareau (University of South Brittany, France), Reda Kadri (Alkante/University of South Brittany, France) 
\item A Family of Distributed Deadlock Avoidance Protocols and their Reachable State Spaces 
\item C\'esar Sanchez (Stanford University, USA), Henny B. Sipma (Stanford University, USA), Zohar Manna (Stanford University, USA) 
\item[TACAS - Automata-Based Model Checking (Chair: Daniel Kroening) ]\item Improved algorithms for the automata based approach to model-checking 
\item Laurent Doyen (EPFL) and Jean-Francois Raskin (Universitat Libre de Bruxelles) 
\item GOAL: A Graphical Tool for Manipulating Buechi Automata and Temporal Formulae 
\item Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu, and Wen-Chin Chan (National Taiwan University) 
\item Faster Algorithms for Finitary Games 
\item Florian Horn (LIAFA, Universite Paris 7) 

\end{description}
\subsubsection{Programme of Thursday, March 29}
\subsubsection*{09:00 - 10:00 SESSION 1 (Thursday)}
\begin{description}
\item[FASE - Invited Talk (Chair: Matt Dwyer) ]\item Software Product Families: Towards Compositionality 
\item Jan Bosch (Nokia, Finland) 

\end{description}
\subsubsection*{10:00 - 10:30 Coffee}
\subsubsection*{10:30 - 12:30 SESSION 2 (Thursday)}
\begin{description}
\item[ESOP - Static Analysis and Abstract Interpretation I (Chair: Sophia Drossopulou) ]\item Modular Shape Analysis for Dynamically Encapsulated Programs 
\item Noam Rinetzky (Tel Aviv University), Arnd Poetzsch-Heffter (Universitat Kaiserslautern), Ganesan Ramalingam (Microsoft Research), Mooly Sagiv (Tel Aviv University) and Eran Yahav (IBM T.J. Watson Research Center) 
\item Static Analysis by Policy Interation on Relational Domains 
\item Stephane Gaubert (INRIA), Eric Goubault (CEA/Saclay), Ankur Taly (IIT Bombay) and Sarah Zennou (CEA/Saclay) 
\item Computing Procedure Summaries for Interprocedural Analysis 
\item Sumit Gulwani (Microsoft Research) and Ashish Tiwari (SRI International) 
\item Small witnesses for abstract interpreation based proofs 
\item Fr\'ed\'eric Besson (Irisa/Inria), Thomas Jensen (Irisa/CNRS) and Tiphaine Turpin (Irisa/Universit\'e de Rennes 1) 
\item[FASE - Specification (Chair: Marsha Chechik) ]\item Precise Specification of Use Case Scenarios 
\item Jon Whittle (George Mason University, USA) 
\item Joint Structural and Temporal Property Specification using Timed Story Sequence Diagrams 
\item Florian Klein (University of Paderborn, Germany), Holger Giese (University of Paderborn, Germany) 
\item SDL Profiles - Formal Semantics and Tool Support 
\item R\"udiger Grammes (University of Kaiserslautern, Germany), Reinhard Gotzhein (University of Kaiserslautern, Germany) 
\item Preliminary design of BML: A Behavioural Interface Specification Language for java bytecode 
\item Lilian Burdy (INRIA Sophia Antipolis, France), Marieke Huisman (INRIA Sophia Antipolis, France), Mariele Pavlova (INRIA Sophia Antipolis, France) 
\item[TACAS - Specification Languages (Chair: Marsha Chechik) ]\item Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based Programs 
\item David Harel and Itai Segall (The Weizmann Institute of Science) 
\item MoToR: The MoDeST Tool Environment 
\item Henrik Bohnenkamp (RWTH Aachen University), Holger Hermanns (Saarland University), and Joost-Pieter Katoen (RWTH Aachen University and University of Twente) 
\item Syntactic Optimizations for PSL Verification 
\item Alessandro Cimatti, Marco Roveri (ITC-irst Trento), and Stefano Tonetta (University of Lugano) 
\item The Heterogeneous Tool Set 
\item Till Mossakowski, Christian Maeder (DFKI Lab and University of Bremen), and Klaus Luettich (SFB/TR 8 and University of Bremen) 

\end{description}
\subsubsection*{12:30 - 14:30 Lunch }
\subsubsection*{14:30 - 15:40 SESSION 3A (Thursday)}
\begin{description}
\item[Unifying Invited Talk (Chair: Jo\~ao Saraiva) ]\item Contract-Driven Development 
\item Bertrand Meyer (ETH Z\"urich, Switzerland) 

\end{description}
\subsubsection*{15:40 - 15:50 Break }
\subsubsection*{15:50 - 16:50 SESSION 3B (Thursday)}
\begin{description}
\item[ESOP - Static Analysis and Abstract Interpretation II (Chair: Sophia Drossopulou) ]\item Interprocedurally analyzing linear inequality relations 
\item Hemut Seidl (Lehrstuhl Seidl, TUM) , Andrea Flexeder (TU Munich) and Michael Petter. (TU Munich) 
\item Precise Fixpoint Computation Through Strategy Iteration 
\item Thomas Gawlitza (Lehrstuhl Seidl, TUM) and Hemut Seidl (Lehrstuhl Seidl, TUM) 
\item[TACAS - Security (Chair: Michael Huth) ]\item Searching for Shapes in Cryptographic Protocols 
\item Shaddin F. Doghmi, Joshua D. Guttman, and F. Javier Thayer (The MITRE Corporation) 
\item Automatic Analysis of the Security of XOR-based Key Management Schemes 
\item Veronique Cortier (Loria and CNRS and INRIA), Gavin Keighren, and Graham Steel (University of Edinburgh) 

\end{description}
\subsubsection*{16:50 - 17:15 Coffee}
\subsubsection*{17:15 - 18:45 SESSION 4 (Thursday)}
\begin{description}
\item[ESOP - Semantic Theories for OO Languages (Chair: Gerard Boudol) ]\item A Complete Guide to the Future 
\item Frank S. de Boer (CWI), Dave Clarke (CWI) and Einar Broch Johnsen (University of Oslo) 
\item The Java Memory Model: Operationally, Denotationally, Axiomatically 
\item Pietro Cenciarelli (University of Rome - ``La Sapienza''), Alexander Knapp (Ludwig-Maximilians University Munich) and Eleonora Sibilio (University of Rome - ``La Sapienza'') 
\item Immutable Objects for a Java-like Language 
\item Christian Haack (Radboud Universiteit, Nijmegen), Erik Poll (Radboud Universiteit, Nijmegen), Jan Schaefer (TU Kaiserslautern) and Aleksy Schubert (Radboud Universiteit, Nijmegen) 
\item[FASE - Services (Chair: Jos\'e Fiadeiro) ]\item A Service Composition Construct to Support Iterative Development 
\item Roy Gronmo (SINTEF, Norway), Michael C. Jaeger (Technical University Berlin, Germany), Andreas Wombacher (University Twente, The Netherlands) 
\item Correlation Patterns in Service-Oriented Architectures 
\item Alistair Barros (SAP Research Centre, Australia), Gero Decker (University of Potsdam, Germany), Marlon Dumas (Queensland University of Technology, Australia), Franz Weber (SAP AG, Germany) 
\item Dynamic Characterization of Web Application Interfaces 
\item Marc Fisher II (University of Nebraska-Lincoln, USA), Sebastian Elbaum (University of Nebraska-Lincoln, USA), Gregg Rothermel (University of Nebraska-Lincoln, USA) 
\item[TACAS - Software and Hardware Verification (Chair: Orna Grumberg) ]\item State of the Union: Type Inference via Craig Interpolation 
\item Ranjit Jhala (UC San Diego), Rupak Majumdar, and Ru-Gang Xu (UC Los Angeles) 
\item Hoare Logic for Realistically Modelled Machine Code 
\item Magnus O. Myreen and Michael J. C. Gordon (University of Cambridge) 
\item VCEGAR: Verilog CounterExample Guided Abstraction Refinement 
\item Himanshu Jain (Carnegie Mellon University), Daniel Kroening (ETH Zuerich), Natasha Sharygina (Carnegie Mellon University and University of Lugano), and Edmund Clarke (Carnegie Mellon University) 

\end{description}
\subsubsection{Programme of Friday, March 30}
\subsubsection*{09:00 - 10:00 SESSION 1 (Friday)}
\begin{description}
\item[ESOP - Invited Talk (Chair: Rocco De Nicola) ]\item Techniques for Contextual Equivalence in Higher-Order, Typed Languages 
\item Andrew Pitts (University of Cambridge, UK) 

\end{description}
\subsubsection*{10:00 - 10:30 Coffee}
\subsubsection*{10:30 - 12:30 SESSION 2 (Friday)}
\begin{description}
\item[ESOP - Process Algebraic Techniques (Chair: Rocco De Nicola) ]\item Scalar Outcomes Suffice for Finitary Probabilistic Testing 
\item Yuxin Deng (University of New South Wales), Rob van Glabbeek (National ICT Australia), Carroll Morgan (University of New South Wales) and Chenyi Zhang (National ICT Australia) 
\item Probabilistic Anonymity via Coalgebraic Simulations 
\item Ichiro Hasuo (Radboud University Nijmegen) and Yoshinobu Kawabe (NTT Corporation) 
\item Proving Distributed Algorithm Correctness using Fault Tolerance Bisimulations 
\item Adrian Francalanza (Imperial College) and Matthew Hennessy (University of Sussex) 
\item A core calculus for a comparative analysis of bio-inspired calculi 
\item Cristian Versari (University of Bologna) 
\item[FASE - Testing (Chair: Reiko Heckel) ]\item A Prioritization Approach for Software Test Cases Based on Bayesian Networks 
\item Siavash Mirarab (University of Waterloo, Canada), Ladan Tahvildari (University of Waterloo, Canada) 
\item Redundancy Based Test-Suite Reduction 
\item Gordon Fraser (Graz University of Technology, Austria), Franz Wotawa (Graz University of Technology, Austria) 
\item Testing Scenario-Based Models 
\item Hillel Kugler (New York University, USA), Michael J. Stern (Yale University, USA), E. Jane Albert Hubbard (New York University, USA) 
\item Integration Testing in Software Product Line Engineering: A Model-based Technique 
\item Sacha Reis (University of Duisburg-Essen, Germany), Andreas Metzger (University of Duisburg-Essen, Germany), Klaus Pohl (Lero, Ireland and University of Limerick, Ireland and University of Duisburg-Essen, Germany) 
\item[TACAS - Decision Procedures and Theorem Provers (Chair: Parosh Abdulla) ]\item Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications 
\item Marcelo F. Frias, Carlos G. Lopez Pombo, and Mariano M. Moscato (Universidad de Buenos Aires and CONICET) 
\item Combined Satisfiability Modulo Parametric Theories 
\item Sava Krstic, Amit Goel, Jim Grundy (Intel Corporation), and Cesare Tinelli (The University of Iowa) 
\item A Groebner Basis Approach to CNF-formulae Preprocessing 
\item Christopher Condrat and Priyank Kalla (University of Utah) 
\item Kodkod: A Relational Model Finder 
\item Emina Torlak and Daniel Jackson (Massachusetts Institute of Technology) 

\end{description}
\subsubsection*{12:30 - 14:30 Lunch }
\subsubsection*{14:30 - 16:30 SESSION 3 (Friday)}
\begin{description}
\item[ESOP - Applicative Programming (Chair: Matthew Hennessy) ]\item A Rewriting Semantics for Type Inference 
\item George Kuan (University of Chicago), David MacQueen (University of Chicago) and Robert Bruce Findler (University of Chicago) 
\item Principal Type Schemes for Modular Programs 
\item Derek Dreyer (Toyota Technological Institute at Chicago) and Matthias Blume (Toyota Technological Institute at Chicago) 
\item A Consistent Semantics of Self-Adjusting Computation 
\item Umut Acar (Toyota Technological Institute at Chicago), Matthias Blume (Toyota Technological Institute at Chicago) and Jacob Donham (Carnegie Mellon University) 
\item Multi-Language Synchronization 
\item Robert Ennals (Intel Research, Berkeley) and David Gay (Intel Research, Berkeley) 
\item[FASE - Analysis (Chair: Tom Maibaum) ]\item Practical reasoning about invocations and implementations of pure methods 
\item \'Ad\'am Darvas (ETH Zurich, Switzerland), K. Rustan M. Leino (Microsoft Research, USA) 
\item Finding Environment Guarantees 
\item Marsha Chechik (University of Toronto, Canada), Mihaela Gheorghiu (University of Toronto, Canada), Arie Gurfinkel (University of Toronto, Canada) 
\item Ensuring Consistency within Distributed Graph Transformation Systems 
\item Ulrike Ranger (RWTH Aachen University, Germany), Thorsten Hermes (RWTH Aachen University, Germany) 
\item Maintaining Consistency in Layered Architectures of Mobile Ad-hoc Networks 
\item Julia Padberg (Technical University Berlin, Germany), Kathrin Hoffmann (Technical University Berlin, Germany), Hartmut Ehrig (Technical University Berlin, Germany), Tony Modica (Technical University Berlin, Germany), Enrico Biermann (Technical University Berlin, Germany), Claudia Ermel (Technical University Berlin, Germany) 
\item[TACAS - Model Checking (Chair: Orna Grumberg) ]\item Bounded Reachability Checking of Asynchronous Systems Using Decision Diagrams 
\item Jinqing Yu, Gianfranco Ciardo (University of California, Riverside), and Gerald Luettgen (University of York) 
\item Model Checking of Tree Logics with Path Equivalences 
\item Rajeev Alur, Pavol Cerny, and Swarat Chaudhuri (University of Pennsylvania) 
\item Uppaal/DMC - Abstraction-based Heuristics for Directed Model Checking 
\item Sebastian Kupferschmid (University of Freiburg), Klaus Drager (Universitat des Saarlandes), Jorg Hoffmann (Digital Enterprise Research Institute, Innsbruck), Berd Finkbeiner (Universitat des Saarlandes), Henning Dierks (OFFIS, Oldenburg), Andreas Podelski (University of Freiburg), Gerd Behrmann (Aalborg University) 
\item mCRL Distributed State Space Generation in Practice 
\item Stefan Blom (Universitat Innsbruck), Jens R. Calame, Bert Lisser (CWI, Amsterdam), Simona Orzan (TU/e, Eindhoven), Jun Pang (Carl von Ossietzky Universitat, Oldenburg), Jaco van de Pol (CWI, Amsterdam and TU/e, Eindhoven), Mohammad Torabi Dashti, and Anton J. Wijs (CWI, Amsterdam) 

\end{description}
\subsubsection*{16:30 - 17:00 Coffee}
\subsubsection*{17:00 - 18:30 SESSION 4 (Friday)}
\begin{description}
\item[ESOP - Types for Systems Properties (Chair: Walid Taha) ]\item Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts 
\item Kohei Suenaga (University of Tokyo) and Naoki Kobayashi (Tohoku University) 
\item Type Reconstruction for an Undecidable System of Refinement Types 
\item Kenneth Knowles (University of California, Santa Cruz) and Cormac Flanagan (University of California, Santa Cruz) 
\item Dependent Types for Low-Level Programming 
\item Jeremy Condit (University of California, Berkeley), Matthew Harren (University of California, Berkeley), Zachary Anderson (University of California, Berkeley), David Gay (Intel Research, Berkeley) and George C. Necula (University of California, Berkeley) 
\item[FASE - Design (Chair: Ant\'onia Lopes) ]\item Towards Normal Design for Safety-Critical Systems 
\item Derek Mannering (General Dynamics, UK), Jon G. Hall (The Open University, UK), Lucia Rapanotti (The Open University, UK) 
\item A Clustering-based Approach for Tracing Object-Oriented Design to Requirement 
\item Xin Zhou (IBM China Research Lab, China), Hui Yu (Peking University, China) 
\item Measuring and Characterizing Crosscutting in Aspect-Based Programs: Basic Metrics and Case Studies 
\item Roberto E. Lopez-Herrejon (University of Oxford, England), Sven Apel (University of Magdeburg, Germany) 
\item[TACAS - Infinite-State Systems (Chair: Michael Huth) ]\item A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes 
\item Ahmed Bouajjani, Yan Jurski, and Mihaela Sighireanu (LIAFA, University of Paris 7) 
\item Unfolding Concurrent Well-Structured Transition Systems 
\item Frederic Herbreteau, Gregoire Sutre, and The Quang Tran (LaBRI, Bordeaux) 
\item Regular Model Checking without Transducers (On Efficient Verification of Parameterized Systems) 
\item Parosh Aziz Abdulla (Uppsala University), Giorgio Delzanno (Universita di Genova), Noomene Ben Henda, and Ahmed Rezine (Uppsala University) 

\end{description}
\section{Workshops}
\\ 
\begin{itemize}
\item \textbf{ACCAT}
, Applied and Computational Category Theory 
\item \textbf{AVIS \emph{(cancelled)}
}
, Sixth International Workshop on Automated Verification of Infinite-State Systems 
\item \textbf{Bytecode}
 - Bytecode Semantics, Verification, Analysis and Transformation 
\item \textbf{COCV}
, Sixth Workshop on Compiler Optimization Meets Compiler Verification 
\item \textbf{FESCA}
, Formal Foundations of Embedded Software and Component-Based Software Architectures 
\item \textbf{FinCo}
, Foundations of Interactive Computation 
\item \textbf{GT-VMT}
, Sixth International Workshop on Graph Transformation and Visual Modeling Techniques 
\item \textbf{HAV}
, Heap Analysis and Verification 
\item \textbf{HFL}
, Hardware design using Functional Languages 
\item \textbf{LDTA}
, Seventh Workshop on Language Descriptions, Tools and Applications 
\item \textbf{MBT}
, Third Workshop on Model Based Testing 
\item \textbf{MOMPES}
, Model-based Methodologies for Pervasive and Embedded Software 
\item \textbf{OpenCert}
, Foundations and Techniques for Open Source Software Certification 
\item \textbf{QAPL}
, Fifth Workshop on Quantitative Aspects of Programming Languages 
\item \textbf{SC}
, Software Composition 
\item \textbf{SLA++P}
, Model-driven High-level Programming of Embedded Systems 
\item \textbf{TERMGRAPH}
, Fourth International Workshop on Computing with Terms and Graphs 
\item \textbf{WITS}
, Seventh Workshop on Issues in the Theory of Security 
 
\end{itemize}
\subsubsection{ACCAT}
\subsubsection*{Applied and Computational Category Theory}


  Category Theory is a well-known powerful mathematical modeling language with a wide area of applications in mathematics and computer science, including especially the semantical foundations of topics in software science and development. Since about 30 years there have been workshops including these topics. More recently, the ACCAT group established by Jochen Pfalzgraf at Linz and Salzburg has begun to study interesting applications of category theory in Geometry, Neurobiology, Cognitive Sciences, and Artificial Intelligence. It is the intention of this ACCAT workshop to bring together leading researchers in these areas with those in Software Science and Development in order to transfer categorical concepts and theories in both directions. 


 \textbf{Contact: }
 Ulrike Prange (uprange@cs.tu-berlin.de) 


 \textbf{URL: }
 \url{http://tfs.cs.tu-berlin.de/workshops/accat2007/} 
\subsubsection{AVIS \emph{(cancelled)}
}
\subsubsection*{Sixth International Workshop on Automated Verification of Infinite-State Systems}


 \emph{This satellite event has been cancelled.}
 
 AVIS is a forum for researchers interested in the application of formal methods for the automatic verification of large practical systems. Model checking, which has found wide application on hardware descriptions, does not scale to practical software systems due to state explosion. For such systems, theorem proving -- a process requiring manual effort and mathematical sophistication to use -- has so far been the only viable alternative. \\ 
 More recently, hybrid techniques have been developed that combine the ease-of-use of model checkers with the power of theorem provers, yielding tools that are less sensitive to the size of the state space (which may be infinite.) AVIS provides a forum for those who are interested in this emerging area of research that has a bright future. 

 \textbf{Contact: }
 Ramesh Bharadwaj (ramesh@itd.nrl.navy.mil) 


 \textbf{URL: }
 \url{http://chacs.nrl.navy.mil/AVIS07} 
\subsubsection{ByteCode}
\subsubsection*{Second Workshop on Bytecode Semantics, Verification, Analysis and Transformation}


  Bytecode, such as produced by e.g. Java and .NET compilers, has become an important topic of interest, both for industry and academia. The industrial interest stems from the fact that bytecode is typically used for the Internet and mobile devices (smartcards, phones, etc.), where security is a major issue. Moreover, bytecode is device-independent and allows dynamic loading of classes, which provides an extra challenge for the application of formal methods. In addition, the unstructuredness of the code and the pervasive presence of the operand stack also provide extra challenges for the analysis of bytecode. This workshop will focus on the latest developments in the semantics, verification, analysis, and transformation of bytecode. Both new theoretical results and tool demonstrations are welcome. 


 \textbf{Contact: }
 Fausto Spoto (fausto.spoto@univr.it) 


 \textbf{URL: }
 \url{http://www.sci.univr.it/~spoto/Bytecode07/} 
\subsubsection{COCV}
\subsubsection*{Sixth International Workshop on Compiler Optimization Meets Compiler Verification}


  COCV provides a forum for researchers and practitioners working on optimizing and verifying compilation, and on related fields such as translation validation, certifying compilation and embedded systems with a special emphasis on hardware verification, formal synthesis methods, correctness aspects in HW/SW co-design, formal verification of hardware/software systems, and practical and industrial applications of formal techniques for exchanging their latest findings, and for plumbing the mutual impact of these fields on each other. By encouraging discussions and co-operations across different, yet related fields, the workshop strives for bridging the gap between the communities, and for stimulating synergies and cross-fertilizations among them. 


 \textbf{Contact: }
 Sabine Glesner (glesner@cs.tu-berlin.de) 


 \textbf{URL: }
 \url{http://pes.cs.tu-berlin.de/cocv2007/} 
\subsubsection{FESCA}
\subsubsection*{Formal Foundations of Embedded Software and Component-Based Software Architectures}


  The aim of this workshop is to bring together researchers from academia and industry interested in formal modeling approaches as well as associated analysis and reasoning techniques with practical benefits for embedded software and component-based software engineering. \\ 
 Recent years has seen the emergence of formal and informal techniques and technologies for the specification and implementation of component-based software architectures. Formal methods have sometimes not kept up with the increasing complexity of software. For instance, a range of new middleware platforms have been developed in both enterprise and embedded systems industries. FESCA aims to address the open question of how formal methods can be applied effectively to these new contexts. 


 \textbf{Contact: }
 Iman Poernomo (iman.poernomo'at symbol'kcl.ac.uk) 


 \textbf{URL: }
 \url{http://palab.dcs.kcl.ac.uk/fesca/} 
\subsubsection{FinCo}
\subsubsection*{Foundations of Interactive Computation}


  Since the 1960's, computation has become increasingly interactive. Concurrent, distributed, reactive, embedded, component-oriented, agent-oriented and service-oriented systems all fundamentally depend on interaction. However, a satisfactory formal foundation of interactive computation, analogous to one that recursive functions, Turing Machines, and lambda-calculus provide for algorithms, is still lacking. Furthermore, the implications of treating interaction as a first-class concept in the process of software design and construction remain to be fully understood. \\ 
 Following the success of FInCo 2005, our goals are to work towards developing a unified conceptual and formal framework for understanding the principles of interaction, establishing language- and domain-independent models for it, and improving the development of software applications and systems through the application of interactive principles and models. 


 \textbf{Contact: }
 Dina Goldin (finco07@cs.brown.edu) 


 \textbf{URL: }
 \url{http://www.cs.brown.edu/sites/finco07/} 
\subsubsection{GT-VMT}
\subsubsection*{Sixth International Workshop on Graph Transformation and Visual Modeling Techniques}


  GT-VMT 2007 is the sixth workshop of a series that serves as a forum for all researchers and practitioners interested in the use of graph-based notation, techniques and tools for the specification, modeling, validation, manipulation and verification of complex systems. Due to the variety of languages and methods used in different domains, the aim of the workshop is to promote engineering approaches that starting from high-level specifications and robust formalizations allow for the design and the implementation of such visual modeling techniques, hence providing effective tool support at the semantic level (e.g., for model analysis, transformation, and consistency management). This year's workshop will have an additional focus on application of graph transformation and visual modeling techniques in engineering, biology, and medicine. 


 \textbf{Contact: }
 Karsten Ehrig (karsten@mcs.le.ac.uk) 


 \textbf{URL: }
 \url{http://www.cs.le.ac.uk/events/GTVMT07/} 
\subsubsection{HAV}
\subsubsection*{Heap Analysis and Verification}


  Accurate and efficient expression, discovery, and verification of the structure of program heap memory is an active research area. Many problems remain open, and therefore many programs remain unverified. We are seeing advances however: Among these are exciting new techniques for analysis and verification of concurrently accessed heap memory, new techniques for interprocedural and modular analysis and verification, and great strides increasing the range of practically applicable analysis and verification techniques. The aim of this workshop is to bring together researchers to exchange and develop new ideas in all aspects of formal analysis and verification for heaps. Submissions are invited from across the full spectrum of basic theoretical work through to applied practical work. 


 \textbf{Contact: }
 Josh Berdine (jjb@microsoft.com) 


 \textbf{URL: }
 \url{http://www.cs.tau.ac.il/~msagiv/hav.html} 
\subsubsection{HFL}
\subsubsection*{Hardware design using Functional Languages}


  More abstract representations and verification techniques are needed to keep up with the ever-increasing complexity of modern hardware designs. We face challenging research problems, many of them related to language design and to ways of modelling circuits at various levels of abstraction. \\ 
 This workshop will bring together researchers in modern functional languages, hardware description languages, high-level modelling and validation, and formal design environments. It aims to present the state of the art, and to spark debate about how to proceed. \\ 
 To achieve the necessary breakthroughs, we must ensure that academics and industrial researchers continue to work together to solve the real challenge of hardware design and verification. A major aim of this workshop is to open the necessary communication channels. 


 \textbf{Contact: }
 Andy Martin (hfl07@hflworkshop.org) 


 \textbf{URL: }
 \url{http://hfl07.hflworkshop.org/} 
\subsubsection{LDTA}
\subsubsection*{Seventh Workshop on Language Descriptions, Tools and Applications}


  The LDTA workshops bring together academic and industrial researchers interested in the field of formal language definitions and language technologies, with an emphasis on tools developed for or with these language definitions. This active research area includes basic approaches such as the analysis, transformation, and generation of programs, the formal analysis of language properties, and the automatic generation of language processing tools. \\ 
 Several specification formalisms like attribute grammars, action semantics, operational semantics, and algebraic approaches have been developed over the years. A goal of LDTA is to increase the use of such formalisms through demonstrations of their practical utility in, among others, the following application domains: component models and modeling languages, re-engineering and re-factoring, aspect-oriented and domain-specific languages, XML processing, visualization and graph transformation, and programming environments, such as Eclipse. 


 \textbf{Contact: }
 Eric Van Wyk (evw@cs.umn.edu) 


 \textbf{URL: }
 \url{http://www.di.uminho.pt/ldta07} 
\subsubsection{MBT}
\subsubsection*{3rd Workshop on Model Based Testing}


  The workshop is devoted to model-based testing of both software and hardware. Model-based testing uses models that describe the behavior of the system under consideration to guide such efforts as test selection and test results evaluation. \\ 
 Model-based testing has gained attention with the popularization of models in software/hardware design and development. Of particular importance are formal models with precise semantics, such as state-based formalisms. Testing with such models allows one to measure the degree of the product's conformance with the model. \\ 
 Techniques to support model-based testing are drawn from diverse areas, like formal verification, model checking, control and data flow analysis, grammar analysis, and Markov decision processes. \\ 
 The intent of this workshop is to discuss the state of the art in theory, application, tools, and industrialization of model-based testing. 


 \textbf{Contact: }
 Bernd Finkbeiner (finkbeiner@cs.uni-sb.de) 


 \textbf{URL: }
 \url{http://react.cs.uni-sb.de/mbt2007/} 
\subsubsection{MOMPES}
\subsubsection*{4th International Workshop on Model-based Methodologies for Pervasive and Embedded Software}


  Model Based Development (MBD) comprises approaches to software development which heaviliy rely on modeling and the systematic transition from models to executable code. One of these approaches is the OMG's Model Driven Architecture (MDA), which is based on the separation between the specification of a system and its implementation using specific platforms. This workshop focuses on the scientific and practical aspects related with the adoption of MDA and other MBD methodologies (notation, process, methods, and tools) for supporting the construction of computer-based systems, and more specifically, pervasive and embedded software. 


 \textbf{Contact: }
 Jo\~ao M. Fernandes (mompes@di.uminho.pt) 


 \textbf{URL: }
 \url{http://www.di.uminho.pt/mompes} 
\subsubsection{OpenCert}
\subsubsection*{Foundations and Techniques for Open Source Software Certification}


  The aim of this workshop is to bring together researchers from academia and industry who are interested in developing techniques for the quality assessment of Open Source Software (OSS), leading to the definition of a complete certification process. \\ 
 The workshop will focus on formal methods and model-based techniques, emphasising on those aspects which are specific to OSS, such as unconventional development, rapid evolution of the code, and huge amount of legacy code. \\ 
 Contributions to the workshop are expected to present foundations, methods, tools and case studies that integrate techniques from different areas such as certification, security, reverse engineering, and formal modeling and verification, in order to overcome the challenges in the quality assessment of OSS. 


 \textbf{Contact: }
 Luis Barbosa (opencert07@di.uminho.pt) 


 \textbf{URL: }
 \url{http://opencert.iist.unu.edu/} 
\subsubsection{QAPL}
\subsubsection*{5th Workshop on Quantitative Aspects of Programming Languages}


  Quantitative aspects of computation are important and sometimes essential in characterising the behaviour and determining the properties of systems. They are related to the use of physical quantities (e.g. time, bandwidth) as well as mathematical quantities (e.g. probabilities) which play a central role in defining models (architectures, protocols, languages, etc.) and methodologies for analysis and verification. \\ 
 The aim of this workshop is to discuss the explicit role of real-time aspects, probabilities, resource consumption, performance parameters, etc. in the design as well the analysis of such systems. The topics covered are transversal to all areas of Computer Science including Languages, Protocols, Architectures, Security, Semantics, Analysis, etc. Particular relevance will be given to the emerging areas of Quantum Computation and Bioinformatics. 


 \textbf{Contact: }
 Alessandro Aldini and Franck van Breugel (qapl07@cse.yorku.ca) 


 \textbf{URL: }
 \url{http://www.cse.yorku.ca/qapl07} 
\subsubsection{SC}
\subsubsection*{Workshop on Software Composition}
 The goal of SC 2007 is to develop a better understanding of how we build and maintain large software systems, and thereby to build the body of knowledge and experience in software composition. The sixth SC symposium will bring together the research and industrial communities to address the challenges of the component-based approach to software development. Suggested topics of interess related to component systems include: \begin{itemize}
\item  Composition and adaptation techniques 
\item  Composition issues in industrial-strength systems 
\item  Composition languages, calculi and type systems 
\item  Composition of active documents 
\item  Compositional web service design and implementation 
\item  Dynamic composition and reconfiguration 
\item  Pervasive computing environments 
\item  Semantics-based composition and analysis 
\item  The role of Aspect-Oriented Software Development in composition 
\item  Verification, validation and testing techniques 
 
\end{itemize}


 \textbf{Contact: }
 Judith Bishop (jbishop@cs.up.ac.za) 


 \textbf{URL: }
 \url{http://ssel.vub.ac.be/sc2007} 
\subsubsection{SLA++P}
\subsubsection*{Model-driven High-level Programming of Embedded Systems}


  SLA++P is dedicated to synchronous languages and the model-driven high-level programming of reactive and embedded systems. Firmly grounded in clean mathematical semantics, synchronous languages are receiving increasing attention in industry ever since they emerged in the 80s. Lustre, Esterel, Signal are now widely and successfully used to program real-time and safety critical applications of commercial scale. At the same time, model-based programming is making its way in other fields of software engineering, often involving cycle-based synchronous paradigms. SLA++P extends the former SLAP workshop series on Synchronous Languages, Applications, and Programming but is not limited to synchronous approaches. It is open to other engineering design techniques with strong semantical foundations to go from high-level description to provable executable code. 


 \textbf{Contact: }
 Michael Mendler (michael.mendler@wiai.uni-bamberg.de) 


 \textbf{URL: }
 \url{http://web.uni-bamberg.de/wiai/gdi/SLAP07/} 
\subsubsection{TERMGRAPH}
\subsubsection*{4th International Workshop on Computing with Terms and Graphs}


  The advantage of computing with graphs rather than terms is that common subexpressions can be shared, improving the efficiency of computations in space and time. Sharing is ubiquitous in implementations of programming languages: many functional, logic, object-oriented and concurrent calculi are implemented using term graphs. Research in term and graph rewriting ranges from theoretical questions to practical implementation issues. Different research areas include: the modelling of first- and higher-order term rewriting by (acyclic or cyclic) graph rewriting, the use of graphical frameworks such as interaction nets and sharing graphs (optimal reduction), rewrite calculi for the semantics and analysis of functional programs, graph reduction implementations of programming languages, graphical calculi modelling concurrent and mobile computations, object-oriented systems, graphs as a model of biological or chemical abstract machines, and automated reasoning and symbolic computation systems working on shared structures. 


 \textbf{Contact: }
 Ian Mackie (ian.mackie@kcl.ac.uk) 


 \textbf{URL: }
 \url{http://www.termgraph.org.uk} 
\subsubsection{WITS}
\subsubsection*{7th International Workshop on Issues in the Theory of Security}


  WITS is the official workshop organized by the IFIP WG 1.7 on ``Theoretical Foundations of Security Analysis and Design$^\prime$$^\prime$, established to promote the investigation on the theoretical foundations of security, discovering and promoting new areas of application of theoretical techniques in computer security and supporting the systematic use of formal techniques in the development of security related applications. The members of WG hold their annual workshop as an open event to which all researchers working on the theory of computer security are invited. This is the seventh meeting of the series, and is organized in cooperation with ACM SIGPLAN (to be confirmed) and the working group FoMSESS of the German Computer Society (GI). There will be proceedings published as ``Issues in the Theory of Security$^\prime$$^\prime$. 


 \textbf{Contact: }
 Riccardo Focardi (\url{http://www.dsi.unive.it/~focardi/}) 


 \textbf{URL: }
 \url{http://www.dsi.unive.it/IFIPWG1}\_7/wits2007.html 
 \\ 
\\ 
\textbf{ FURTHER INFORMATION AND ENQUIRIES }


  \url{http://www.di.uminho.pt/etaps07} \\ 
 etaps07@di.uminho.pt \\ 
 Luis Barbosa \\ 
 Joost Visser \\ 
 ETAPS 2007 Satellite Events Co-chairs \\ 
 lsb@di.uminho.pt, joost.visser@di.uminho.pt \\ 
 


  
 \subsection{Programme of ACCAT at ETAPS 2007}
\subsubsection{(Applied and Computational Category Theory)}
\subsubsection{Sunday, March 25, room: CP2-103}
\\ 
\subsubsection*{09:00 - 10:15 SESSION 1}
\begin{description}
\item Introduction 
\item Generalized Sketches - A Universal Pattern for Diagrammatic Specification 
\item Uwe Wolter 
\item Dynamics and Cohesion in Finite Toposes 
\item William Lawvere 

\end{description}
\subsubsection*{10:15 - 11:00 Coffee Break}
\subsubsection*{11:00 - 12:30 SESSION 2}
\begin{description}
\item Normalized Coalgebras for Dynamic Bisimilarity 
\item Ugo Montanari 
\item Structured Co-spans: Algebraic Modelling of Interaction Protocols 
\item Jos\'e Fiadeiro 
\item Iterative Algebras 
\item Jiri Adamek 

\end{description}
\subsubsection*{12:30 - 14:00 Lunch}
\subsubsection*{15:00 - 16:00 SESSION 3}
\begin{description}
\item A Categorical Model of Computation for Graph Transformation: True Concurrency and Logic 
\item Reiko Heckel 
\item Adhesive High-Level Replacement Systems with Negative Application Conditions 
\item Leen Lambers 
\item Composing DPO Transformations with Borrowed Context 
\item Paolo Baldan 
\item Algebraic High-Level Systems as Weak Adhesive HLR Categories 
\item Ulrike Prange 

\end{description}
\subsubsection*{16:00 - 16:30 Coffee Break}
\subsubsection*{16:30 - 18:00 SESSION 4}
\begin{description}
\item Categories in the Design of Aldor 
\item Stephen Watt 
\item (tba) 
\item Vladimiro Sassone 
\item (tba) 
\item Jochen Pfalzgraf 

\end{description}
\subsubsection*{18:45 SOCIAL EVENT}
\begin{description}
\item[Joint Workshops Pre-Conference Dinner ]\item Dinner at Bom Jesus \emph{(Shutle departure from Campus Gualtar)}
 

\end{description}
\\ 
\subsubsection*{Further ETAPS 2007 Programme Information:}
\begin{itemize}
\item Programme Overview
\item Main Conferences: Complete Programme, CC, ESOP, FASE, FOSSACS, TACAS 
\item Workshops:  Bytecode, COCV, FESCA, FinCo, GT-VMT, HAV, HFL, LDTA, MBT, MOMPES, OpenCert, QAPL, SC, SLA++P, TERMGRAPH, WITS, 
\item Tutorials: Stratego/XT, SoftwGen Mobius 
 
\end{itemize}
ETAPS 2007 | Top | HTML 4.01 | Last Update: 2007-03-13  \subsection{Programme of Bytecode at ETAPS 2007}
\subsubsection{(Second Workshop on Bytecode Semantics, Verification, Analysis and Transformation)}
\subsubsection{Saturday, March 31, room: CP2-103}
\subsubsection*{09:00 - 10:30 SESSION 1}
\begin{description}
\item[Session Chair: Marieke Huisman ]\item Invited Talk: Modular verification of object invariants in Spec\# 
\item Peter M\"uller (ETH Zurich) 
\item Type Systems for optimising Stack-based Code 
\item Tarmo Uustalu and Ando Saabas (Tallinn University of Technology, Estonia) 

\end{description}
\subsubsection*{10:30 - 11:00 Coffee Break}
\subsubsection*{11:00 - 12:30 SESSION 2}
\begin{description}
\item Proving Resource Consumption of Low-level and Programs using Automated Theorem Provers 
\item Jaroslav Sevcik (University of Edinburgh, UK) 
\item Formal Translation of Bytecode into BoogiePL 
\item Hermann Lehner and Peter M\"uller (ETH, Zurich, Switzerland) 
\item Bytecode Rewriting in Tom 
\item Emilie Balland, Pierre-Etienne Moreau and Antoine Reilles (Loria, France) 

\end{description}
\subsubsection*{12:30 - 14:00 Lunch}
\subsubsection*{14:00 - 16:00 SESSION 3}
\begin{description}
\item[Session Chair: Peter M\"uller ]\item Translate One, Analyze Many: Leveraging the Microsoft Intermediate Language and Source Code Transformation for Model Checking 
\item Jesse McGeachie and Juergen Dingel (Queen's University, Canada) 
\item Practical Assessment of Cost Analysis for Java Bytecode 
\item Samir Genaim, Puri Arenas, Damiano Zanardini, German Puebla and Elvira Albet (Universidad Polit\'ecnica de Madrid, Universidad Complutense de Madrid, Spain) 
\item MMC: the Mono Model Checker 
\item Theo Ruys and Niels H.M. Aan de Brugh (University of Twente, The Netherlands) 
\item Improving the Decompilation of Java Bytecode to Prolog by Partial Evaluation 
\item Miguel Gomez-Zamalloa, Elvira Albert and German Puebla (Universidad Polit\'ecnica de Madrid, Universidad Complutense de Madrid, Spain) 

\end{description}
\subsubsection*{16:00 - 16:30 Coffee Break}
\subsubsection*{16:30 - 17:30 SESSION 4}
\begin{description}
\item[Session Chair: Fausto Spoto ]\item Computing SSA Form with Matrices 
\item Quan Nguyen and Bernhard Scholz (University of New South Wales, University of Sydney, Australia) 
\item An Efficient, Parametric Fixpoint Algorithm for Incremental Analysis of Java Bytecode 
\item Mario M\'endez, Jorge Navas and Manuel Hermenegildo (University of New Mexico, USA) 

\end{description}
\subsubsection*{18:45 SOCIAL EVENT}
\begin{description}
\item[Joint Workshops Post-Conference Dinner ]\item Dinner at Pousada Santa Maria de Bouro \emph{(Shutle departure from Campus Gualtar)}
 

\end{description}
\\ 
\subsubsection*{Further ETAPS 2007 Programme Information:}
\begin{itemize}
\item Programme Overview
\item Main Conferences: Complete Programme, CC, ESOP, FASE, FOSSACS, TACAS 
\item Workshops: ACCAT,  COCV, FESCA, FinCo, GT-VMT, HAV, HFL, LDTA, MBT, MOMPES, OpenCert, QAPL, SC, SLA++P, TERMGRAPH, WITS, 
\item Tutorials: Stratego/XT, SoftwGen Mobius 
 
\end{itemize}
ETAPS 2007 | Top | HTML 4.01 | Last Update: 2007-03-13  \subsection{Programme of COCV at ETAPS 2007}
\subsubsection{(Compiler Optimization meets Compiler Verification)}
\subsubsection{Sunday, March 25, room: CP2-108}
\\ 
\subsubsection*{09:00 - 10:30 SESSION 1}
\begin{description}
\item[Opening ]\item Jens Knoop, Vienna University of Technology 
\item[Invited Talk ]\item High-Level vs. RTL Equivalence Checking: Why the Next Big Success of Formal Verification Needs COCV 
\item Alan Hu, University of British Columbia, Canada 

\end{description}
\subsubsection*{10:30 - 11:00 Coffee Break}
\subsubsection*{11:00 - 12:00 SESSION 2}
\begin{description}
\item Specify, Compile, Run: Hardware from PSL 
\item Bloem, Galler, Jobstmann, Piterman, Pnueli, Weiglhofer (Graz University of Technology, Austria; EPFL Lausanne, Switzerland; Weizmann Institute, Israel) 

\end{description}
\subsubsection*{12:30 - 14:00 Lunch}
\subsubsection*{14:00 - 16:00 SESSION 3}
\begin{description}
\item Distilling Programs for Verification 
\item Geoff Hamilton (Dublin City University, Ireland) 
\item On-the-Fly Data Flow Analysis based on Verification Technology 
\item Mar\`Ia del Mar Gallardo, Christophe Joubert and Pedro Merino (University of M\'alaga, Spain) 

\end{description}
\subsubsection*{16:00 - 16:30 Coffee Break}
\subsubsection*{16:30 - 18:00 SESSION 4}
\begin{description}
\item Generating Java Compiler Optimizers Using Bidirectional CTL 
\item Ling Fang and Masataka Sassa (Tokyo Institute of Technology, Japan) 
\item A Certifying Code Generation Phase 
\item Jan Olaf Blech and Arnd Poetzsch-Heffter (University of Kaiserslautern, Germany) 

\end{description}
\subsubsection*{16:30 - 18:00 Closure}
\subsubsection*{18:45 SOCIAL EVENT}
\begin{description}
\item[Joint Workshops Pre-Conference Dinner ]\item Dinner at Bom Jesus \emph{(Shutle departure from Campus Gualtar)}
 

\end{description}
\\ 
\subsubsection*{Further ETAPS 2007 Programme Information:}
\begin{itemize}
\item Programme Overview
\item Main Conferences: Complete Programme, CC, ESOP, FASE, FOSSACS, TACAS 
\item Workshops: ACCAT, Bytecode,  FESCA, FinCo, GT-VMT, HAV, HFL, LDTA, MBT, MOMPES, OpenCert, QAPL, SC, SLA++P, TERMGRAPH, WITS, 
\item Tutorials: Stratego/XT, SoftwGen Mobius 
 
\end{itemize}
ETAPS 2007 | Top | HTML 4.01 | Last Update: 2007-03-13  \subsection{Programme of FESCA at ETAPS 2007}
\subsubsection{(Formal Foundations of Embedded Software and Component-Based Software Architectures)}
\subsubsection{Saturday, March 24, room: CP2-108}
\subsubsection*{09:00 - 10:30 SESSION 1}
\begin{description}
\item[Introductory Remarks ]\item[Invited Talk ]\item SENSORIA: Semantic-based Development of Service-Oriented Systems 
\item Martin Wirsing (LMU) 

\end{description}
\subsubsection*{10:30 - 11:00 Coffee Break}
\subsubsection*{11:00 - 12:30 SESSION 2}
\begin{description}
\item[Formal models for component-based assembly ]\item A True-Concurrent Interpretation of Behavioural Scenarios 
\item Sotiris Moschoyiannis, Paul Krause and Michael Shields 
\item Trustworthy interface compliancy: data model adaptation using B refinement 
\item Samuel Colin, Arnaud Lanoix, Jeanine Souquieres 
\item Towards Component Verification in the Generic Component Framework 
\item Julia Padberg, Hartmut Ehrig, Fernando Orejas 

\end{description}
\subsubsection*{12:30 - 14:00 Lunch}
\subsubsection*{14:00 - 16:00 SESSION 3}
\begin{description}
\item[Behavioural models ]\item DeSpec: Modeling the Windows Driver Environment 
\item Tomas Matousek and Pavel Jezek 
\item WCET Analysis of Data Dependent, Component Oriented, Embedded Software Systems 
\item Peter Szulman 
\item Composing Modal Properties of Programs with Procedures 
\item Marieke Huisman, Dilian Gurov 

\end{description}
\subsubsection*{16:00 - 16:30 Coffee Break}
\subsubsection*{16:30 - 17:30 SESSION 4}
\begin{description}
\item[Contractual runtime verification ]\item A Formal Semantics for a Quality of Service Contract Language 
\item Fabricio Chalub, Alexandre Sztajnberg 
\item Executable Contracts for Incremental Prototypes of Embedded Systems 
\item Lionel Morel and Louis Mandel 

\end{description}
\subsubsection*{17:30 Concluding Remarks}
\\ 
\subsubsection{Sunday, March 25}
\\ 
\subsubsection*{18:45 SOCIAL EVENT}
\begin{description}
\item[Joint Workshops Pre-Conference Dinner ]\item Dinner at Bom Jesus \emph{(Shutle departure from Campus Gualtar)}
 

\end{description}
\\ 
\subsubsection*{Further ETAPS 2007 Programme Information:}
\begin{itemize}
\item Programme Overview
\item Main Conferences: Complete Programme, CC, ESOP, FASE, FOSSACS, TACAS 
\item Workshops: ACCAT, Bytecode, COCV,  FinCo, GT-VMT, HAV, HFL, LDTA, MBT, MOMPES, OpenCert, QAPL, SC, SLA++P, TERMGRAPH, WITS, 
\item Tutorials: Stratego/XT, SoftwGen Mobius 
 
\end{itemize}
ETAPS 2007 | Top | HTML 4.01 | Last Update: 2007-03-13  \subsection{Programme of GT-VMT at ETAPS 2007}
\subsubsection{(Sixth International Workshop on Graph Transformation and Visual Modeling Techniques)}
\subsubsection{Saturday, March 31, room: CP2-101}
\subsubsection*{09:00 - 10:30 SESSION 1}
\begin{description}
\item[Opening ]\item[Invited Talk ]\item Membrane Computing [and Graph Transformation] 
\item Gheorghe Paun (Romanian Academy and Sevilla University, Spain) 

\end{description}
\subsubsection*{10:30 - 11:00 Coffee Break}
\subsubsection*{11:00 - 12:30 SESSION 2}
\begin{description}
\item[Verification and Model Transformation ]\item Rule-Level Verification of Business Process Transformations using CSP 
\item D\'enes Bisztray, Reiko Heckel 
\item Bisimulation Verification for the DPO Approach with Borrowed Contexts 
\item Guilherme Rangel, Barbara K\"onig, Hartmut Ehrig 
\item Transforming Collaborative Service Specifications into Efficiently Executable State Machines 
\item Frank Alexander Kraemer, Peter Herrmann 

\end{description}
\subsubsection*{12:30 - 14:15 Lunch}
\subsubsection*{14:15 - 16:00 SESSION 3}
\begin{description}
\item[Pattern Matching ]\item Ensuring Containment Constraints in Graph-based Model Transformation Approaches (Short Talk) 
\item Christian K\"ohler, Holger Lewin, Gabriele Taentzer 
\item Generic Search Plans for Matching Advanced Graph Patterns 
\item \'Akos Horv\'ath, Gergely Varr\'o, D\'aniel Varr\'o 
\item A Query Language With the Star Operator 
\item Johan Lindqvist, Torbj\"orn Lundkvist, Ivan Porres 
\item Triple Patterns: Compact Specifications for the Generation of Operational Triple Graph Grammar Rules 
\item Juan de Lara, Esther Guerra, Paolo Bottoni 

\end{description}
\subsubsection*{16:00 - 16:30 Coffee Break}
\subsubsection*{16:30 - 18:00 SESSION 4}
\begin{description}
\item[Graph Transformation Language Operations ]\item A Subgraph Operator for Graph Transformation Languages 
\item Daniel Balasubramanian, Anantha Narayanan, Sandeep Neema, Feng Shi, Ryan Thibodeaux, Gabor Karsai 
\item Adding Recursion to Graph Transformation 
\item Esther Guerra, Juan de Lara 
\item Visual Programming with Recursion Patterns in Interaction Nets 
\item Ian Mackie, Jorge Sousa Pinto, Miguel Vila\c{c}a 
\item Simulating Multi-graph Transformations Using Simple Graphs (Short Talk) 
\item Frank Hermann, Harmen Kastenberg, Iovka Boneva, Arend Rensink 

\end{description}
\subsubsection*{18:45 SOCIAL EVENT}
\begin{description}
\item[Joint Workshops Post-Conference Dinner ]\item Dinner at Pousada Santa Maria de Bouro \emph{(Shutle departure from Campus Gualtar)}
 

\end{description}
\\ 
\subsubsection{Sunday, April 1, room: CP2-101}
\\ 
\subsubsection*{09:00 - 10:30 SESSION 1}
\begin{description}
\item[Invited Talk ]\item (to be announced)  

\end{description}
\subsubsection*{10:30 - 11:00 Coffee Breaks}
\subsubsection*{11:00 - 12:30 SESSION 2}
\begin{description}
\item[Application of Graph Transformations ]\item Evaluating Workflow Definition Language Revisions with Graph-Based Tools 
\item Ren\'e W\"orzberger, Markus Heller, Frank H\"a"sler 
\item Graph Based Engineering Systems - A Family Of Software Applications And their Underlying Framewor (Short Talk) 
\item Gregor Wrobel, Ralf-Erik Ebert, Matthias Ple"sow 
\item Imposing Hierarchy on a Graph (Short Talk) 
\item Brendan Sheehan, Benoit Gaudin, Aaron Quigley 
\item The Jury is still out: A Comparison of AGG, Fujaba, and PROGRES (Short Talk) 
\item Ulrike Ranger, Christian Fu"s, Christof Mosler, Erhard Schultchen 

\end{description}
\subsubsection*{12:30 - 14:15 Lunch}
\subsubsection*{14:15 - 16:00 SESSION 3}
\begin{description}
\item[Working Groups ]\item Building of Working Groups 
\item Discussion in Working Groups 
\item General Discussion of the Results 
\item[Closing ]
\end{description}
\\ 
\subsubsection*{Further ETAPS 2007 Programme Information:}
\begin{itemize}
\item Programme Overview
\item Main Conferences: Complete Programme, CC, ESOP, FASE, FOSSACS, TACAS 
\item Workshops: ACCAT, Bytecode, COCV, FESCA, FinCo,  HAV, HFL, LDTA, MBT, MOMPES, OpenCert, QAPL, SC, SLA++P, TERMGRAPH, WITS, 
\item Tutorials: Stratego/XT, SoftwGen Mobius 
 
\end{itemize}
ETAPS 2007 | Top | HTML 4.01 | Last Update: 2007-03-13  \subsection{Programme of HAV at ETAPS 2007}
\subsubsection{(Heap Analysis and Verification)}
\subsubsection{Sunday, March 25, room: CP2-104}
\\ 
\subsubsection*{09:00 - 10:30 SESSION 1}
\begin{description}
\item Footprint Analysis: A Shape Analysis that Discovers Preconditions (Invited Lecture) 
\item Hongseok Yang 
\item Proof Systems for Inductive Reasoning in the Logic of Bunched Implications 
\item James Brotherston 

\end{description}
\subsubsection*{10:30 - 11:00 Coffee Break}
\subsubsection*{11:00 - 12:30 SESSION 2}
\begin{description}
\item A Logic of Reachable Patterns (Invited Lecture) 
\item Greta Yorsh 
\item Verifying Complex Properties using Symbolic Shape Analysis 
\item Thomas Wies, Viktor Kuncak, Karen Zee, Martin Rinard and Andreas Podelski 

\end{description}
\subsubsection*{12:30 - 14:00 Lunch}
\subsubsection*{14:00 - 16:00 SESSION 3}
\begin{description}
\item Alias Control with Universe Types (Invited Lecture) 
\item Peter M\"uller 
\item Inferring Local (Non-)Aliasing and Strings for Memory Safety 
\item Yannick Moy and Claude March\'e 
\item Reasoning about Sequences of Memory States 
\item Brochenin R\'emi, Demri St\'ephane and Lozes \'Etienne 

\end{description}
\subsubsection*{16:00 - 16:30 Coffee Break}
\subsubsection*{16:30 - 18:00 SESSION 4}
\begin{description}
\item Liveness of Heap Data for Functional Programs 
\item Amey Karkare, Uday Khedker and Amitabha Sanyal 
\item Separation Analysis for Deductive Verification 
\item Thierry Hubert and Claude March\'e 
\item Verifying Concurrent List-Manipulating Programs by LTL Model Checking 
\item Stefan Rieger, Thomas Noll and Joost-Pieter Katoen 
\item Towards Regional Logic (Invited Lecture) 
\item David Naumann 

\end{description}
\subsubsection*{18:45 SOCIAL EVENT}
\begin{description}
\item[Joint Workshops Pre-Conference Dinner ]\item Dinner at Bom Jesus \emph{(Shutle departure from Campus Gualtar)}
 

\end{description}
\\ 
\subsubsection*{Further ETAPS 2007 Programme Information:}
\begin{itemize}
\item Programme Overview
\item Main Conferences: Complete Programme, CC, ESOP, FASE, FOSSACS, TACAS 
\item Workshops: ACCAT, Bytecode, COCV, FESCA, FinCo, GT-VMT,  HFL, LDTA, MBT, MOMPES, OpenCert, QAPL, SC, SLA++P, TERMGRAPH, WITS, 
\item Tutorials: Stratego/XT, SoftwGen Mobius 
 
\end{itemize}
ETAPS 2007 | Top | HTML 4.01 | Last Update: 2007-03-13  \subsection{Programme of HFL at ETAPS 2007}
\subsubsection{(Hardware design using Functional Languages)}
\subsubsection{Saturday, March 24, room: CP2-110}
\subsubsection*{09:00 - 10:30 SESSION 1}
\begin{description}
\item Introducing Scheduling Primitives and Derived Interfaces in Bluespec 
\item Arvind, Nirav Dave, and Michael Pellauer (MIT) 
\item Declarative Programming Techniques for Many-Core Architectures 
\item Satnam Singh (Microsoft Research Cambridge) 

\end{description}
\subsubsection*{10:30 - 11:00 Coffee Break}
\subsubsection*{11:00 - 12:30 SESSION 2}
\begin{description}
\item Searching for prefix networks to fit in a context using a lazy functional programming language 
\item Mary Sheeran (Chalmers) 
\item The E Language 
\item Robert S. Boyer and Warren A. Hunt, Jr. (University of Texas) 

\end{description}
\subsubsection*{12:30 - 14:30 Lunch and time for discussion}
\subsubsection*{14:30 - 16:00 SESSION 3}
\begin{description}
\item A framework for designing hardware in Ocaml 
\item Andrew K. Martin and Ahmed Gheith (IBM) 
\item High-Level Micro-Architectural Transformations and Cycle-Accurate High-Level Models 
\item Carl-Johan H. Seger (Intel) 

\end{description}
\subsubsection*{16:00 - 16:30 Coffee Break}
\subsubsection*{16:30 - 18:00 SESSION 4}
\begin{description}
\item Functional Programming for Hardware Definition, Verification and Modelling 
\item Nathan Chong and Samin Ishtiaq (ARM) 
\item Program Transformation for Functional Circuit Descriptions 
\item Manfred Schmidt-Schau"s and David Sabel (Johann Wolfgang Goethe-Universit"st) 

\end{description}
\\ 
\subsubsection{Sunday, March 25, room: CP2-110}
\\ 
\subsubsection*{09:00 - 10:30 SESSION 1}
\begin{description}
\item Embedded Hardware Description Languages: Exploring the Design Space 
\item Koen Claessen (Chalmers) and Gordon Pace (University of Malta) 
\item Lightweight Relational Programming for Wired 
\item Matthew Naylor (University of York), Emil Axelsson (Chalmers), and Colin Runciman (University of York) 

\end{description}
\subsubsection*{10:30 - 11:45 Coffee Break and Demos}
\subsubsection*{11:45 - 12:30 SESSION 2}
\begin{description}
\item Towards Automatically Compiling Efficient FPGA Hardware 
\item Jean Baptiste Note and Jean Vuillemin (Ecole Normale Sup\'erieure Paris) 

\end{description}
\subsubsection*{12:30 - 14:30 Lunch and time for discussion}
\subsubsection*{14:30 - 16:00 SESSION 3}
\begin{description}
\item Design Principles for Hardware Description 
\item Tim Sheard (Portland State University) 
\item Hardware descriptions as two-level computations 
\item Walid Taha, Yousra Alkabani, Cherif Andraos, Jennifer Gillenwater, Gregory Malecha and Angela Yun Zhu (Rice University) and Jim Grundy and John O'Leary (Intel) 

\end{description}
\subsubsection*{15:15 - 16:30 Coffee, demos, planning of next workshop}
\subsubsection*{18:45 SOCIAL EVENT}
\begin{description}
\item[Joint Workshops Pre-Conference Dinner ]\item Dinner at Bom Jesus \emph{(Shutle departure from Campus Gualtar)}
 

\end{description}
\\ 
\subsubsection*{Further ETAPS 2007 Programme Information:}
\begin{itemize}
\item Programme Overview
\item Main Conferences: Complete Programme, CC, ESOP, FASE, FOSSACS, TACAS 
\item Workshops: ACCAT, Bytecode, COCV, FESCA, FinCo, GT-VMT, HAV,  LDTA, MBT, MOMPES, OpenCert, QAPL, SC, SLA++P, TERMGRAPH, WITS, 
\item Tutorials: Stratego/XT, SoftwGen Mobius 
 
\end{itemize}
ETAPS 2007 | Top | HTML 4.01 | Last Update: 2007-03-13  \subsection{Programme of LDTA at ETAPS 2007}
\subsubsection{(Seventh Workshop on Language Descriptions, Tools and Applications)}
\subsubsection{Sunday, March 25, room: CP2-111}
\\ 
\subsubsection*{09:00 - 10:30 SESSION 1}
\begin{description}
\item[Welcome and Introduction ]\item[Invited Talk ]\item Collaboration-Based Composition of Languages 
\item Uwe A"smann 
\item[Research Talk ]\item Language Parametric Module Management 
\item Paul Klint, Taeke Kooiker, Jurgen Vinju 

\end{description}
\subsubsection*{10:30 - 11:00 Coffee Break}
\subsubsection*{11:00 - 12:30 SESSION 2}
\begin{description}
\item[Research Talk ]\item Fusing a Transformation Language with an Open Compiler 
\item Karl Trygve Kalleberg, Eelco Visser 
\item[Experience Report ]\item Implementing a Domain-Specific Language using Stratego/XT 
\item Leonard Hamey, Shirley Goldrei 
\item[Tool Demonstration ]\item Spoofax: An Interactive Development Environment for Program Transformation with Stratego/XT 
\item Karl Trygve Kalleberg, Eelco Visser 

\end{description}
\subsubsection*{12:30 - 14:00 Lunch}
\subsubsection*{14:00 - 16:00 SESSION 3}
\begin{description}
\item[Research Talk ]\item SPPF-Style Parsing From Earley Recognisers 
\item Elizabeth Scott 
\item[Experience Report ]\item An Experimental Ambiguity Detection Tool 
\item Sylvain Schmitz 
\item[Research Talk ]\item Grammar Engineering Support for Precedence Rule Recovery and Compatibility Checking 
\item Eric Bouwers, Martin Bravenboer, Eelco Visser 
\item[Tool Demonstration ]\item SdfMetz: Extraction of Metrics and Graphs From Syntax Definitions 
\item Tiago Alves, Joost Visser 

\end{description}
\subsubsection*{16:00 - 16:30 Coffee Break}
\subsubsection*{16:30 - 18:15 SESSION 4}
\begin{description}
\item[Research Talk ]\item Silver: an Extensible Attribute Grammar System 
\item Eric Van Wyk, Derek Bodin, Jimin Gao, Lijesh Krishnan 
\item[Experience Report ]\item Development of a Modelica Compiler using JastAdd 
\item Johan {\AA}kesson, Torbj\"orn Ekman, G\"orel Hedin 
\item[Tool Demonstration ]\item A Domain-Specific Language Debugging Framework Demonstration 
\item Hui Wu, Jeff Gray, Marjan Mernik 
\item[Discussion and Closing ]
\end{description}
\subsubsection*{18:45 SOCIAL EVENT}
\begin{description}
\item[Joint Workshops Pre-Conference Dinner ]\item Dinner at Bom Jesus \emph{(Shutle departure from Campus Gualtar)}
 

\end{description}
\\ 
\subsubsection*{Further ETAPS 2007 Programme Information:}
\begin{itemize}
\item Programme Overview
\item Main Conferences: Complete Programme, CC, ESOP, FASE, FOSSACS, TACAS 
\item Workshops: ACCAT, Bytecode, COCV, FESCA, FinCo, GT-VMT, HAV, HFL,  MBT, MOMPES, OpenCert, QAPL, SC, SLA++P, TERMGRAPH, WITS, 
\item Tutorials: Stratego/XT, SoftwGen Mobius 
 
\end{itemize}
ETAPS 2007 | Top | HTML 4.01 | Last Update: 2007-03-13  \subsection{Programme of OpenCert at ETAPS 2007}
\subsubsection{(Foundations and Techniques for Open Source Software Certification)}
\subsubsection{Saturday, March 31, room: CP2-110}
\subsubsection*{09:00 - 10:30 SESSION 1}
\begin{description}
\item Aspects of OSS Certification 
\item B. Aichernig, TU Graz, Austria 
\item Towards a Quality Model for OSS 
\item S.A. Shaikh \& A. Cerone, UNU-IIST, Macao 

\end{description}
\subsubsection*{10:30 - 11:00 Coffee Break}
\subsubsection*{11:00 - 12:30 SESSION 2}
\begin{description}
\item A System to Understand Programs Written in C Language by Code Annotation 
\item M. Beron, B. Henriques, Univ. of Minho; M. Varanda, Polytechnic Inst. Braganca, Portugal; R. Uzal, Univ. of San Luis, Argentina 
\item Slicing Techniques and Program Calculi in OSS Certification 
\item N. Rodrigues, L. Barbosa, J.N. Oliveira Univ. Minho, Portugal 

\end{description}
\subsubsection*{12:30 - 14:00 Lunch}
\subsubsection*{14:00 - 15:30 SESSION 3}
\begin{description}
\item Linux Certification 
\item A.K. Petrenko, ISPRAS, Russia 
\item OSS Operating Systems for Critical Avionics Infrastructure: A survey on quality and security certification 
\item D. von Oheimb, Siemens, Germany 

\end{description}
\subsubsection*{15:30 - 16:00 Coffee Break}
\subsubsection*{16:00 - 18:30 SESSION 4}
\begin{description}
\item Position Talk on the OSS Certification Process 
\item P.T. Breuer \& S. Pickin, Univ. Carlos III Madrid, Spain 
\item A Perspective on OSS Certification 
\item J. Visser, SIG, The Netherlands 
\item Short Position Statements and Discussion 

\end{description}
\subsubsection*{18:45 SOCIAL EVENT}
\begin{description}
\item[Joint Workshops Post-Conference Dinner ]\item Dinner at Pousada Santa Maria de Bouro \emph{(Shutle departure from Campus Gualtar)}
 

\end{description}
\\ 
\subsubsection*{Further ETAPS 2007 Programme Information:}
\begin{itemize}
\item Programme Overview
\item Main Conferences: Complete Programme, CC, ESOP, FASE, FOSSACS, TACAS 
\item Workshops: ACCAT, Bytecode, COCV, FESCA, FinCo, GT-VMT, HAV, HFL, LDTA, MBT, MOMPES,  QAPL, SC, SLA++P, TERMGRAPH, WITS, 
\item Tutorials: Stratego/XT, SoftwGen Mobius 
 
\end{itemize}
ETAPS 2007 | Top | HTML 4.01 | Last Update: 2007-03-13  \subsection{Programme of QAPL at ETAPS 2007}
\subsubsection{(Fifth Workshop on Quantitative Aspects of Programming Languages)}
\subsubsection{Saturday, March 24, room: CP2-105}
\subsubsection*{10:55 - 12:30 SESSION 1}
\begin{description}
\item[Welcome ]\item[Invited Talk ]\item Nondeterminism in Quantitative Analysis of Probabilistic Systems 
\item Roberto Segala (University of Verona, Italy) 
\item[Paper Presentation: ]\item Keeping Secrets in Resource Aware Components 
\item Tom Chothia (CWI, The Netherlands), Jun Pang (University of Oldenburg, Germany) and Mohammad Torabi Dashti (CWI, The Netherlands) 

\end{description}
\subsubsection*{12:30 - 14:30 Lunch}
\subsubsection*{14:30 - 16:00 SESSION 2}
\begin{description}
\item[Invited Talk ]\item Artificial Biochemistry 
\item Luca Cardelli (Microsoft Research, UK) 
\item[Paper Presentation: ]\item Stochastic Concurrent Constraint Programming and Differential Equations 
\item Luca Bortolussi (University of Trieste, Italy) and Alberto Policriti (University of Udine, Italy) 

\end{description}
\subsubsection*{16:00 - 16:30 Coffee Break}
\subsubsection*{16:30 - 18:00 SESSION 3}
\begin{description}
\item[Paper Presentations: ]\item On Probabilistic Techniques for Data Flow Analysis 
\item Alessandra Di Pierro, Chris Hankin and Herbert Wiklicky (Imperial College London, UK) 
\item Probabilistic Pi-Calculus and Event Structures 
\item Daniele Varacca (University of Paris 7, France) and Nobuko Yoshida (Imperial College London, UK) 
\item Probabilistic Barbed Congruence 
\item Yuxin Deng (Shanghai Jiao Tong University, China) and Wenjie Du (Shanghai Normal University, China) 

\end{description}
\\ 
\\ 
\subsubsection{Sunday, March 25, room: CP2-105}
\\ 
\subsubsection*{09:30 - 10:30 SESSION 1}
\begin{description}
\item[Invited Talk ]\item Approximate Reasoning for Time and Probabilities 
\item Radha Jagadeesan (DePaul University, USA) 

\end{description}
\subsubsection*{10:30 - 11:00 Coffee Break}
\subsubsection*{11:00 - 12:30 SESSION 2}
\begin{description}
\item[Paper Presentations: ]\item Modelling Multicast QoS Routing by using Best-Tree Search in And-or Graphs and Soft Constraint Logic Programming 
\item Stefano Bistarelli (University of Pescara, Italy), Ugo Montanari (University of Pisa, Italy), Francesca Rossi (University of Padova, Italy) and Francesco Santini (IMT Lucca, Italy) 
\item Exogenous Probabilistic Computation Tree Logic 
\item Pedro Baltazar, Paulo Mateus (University of Lisbon, Portugal), Rajagopal Nagarajan and Nikolaos Papanikolaou (University of Warwick, UK) 

\end{description}
\subsubsection*{12:30 - 14:30 Lunch}
\subsubsection*{14:30 - 16:00 SESSION 3}
\begin{description}
\item[Paper Presentations: ]\item Stochastic Modelling of Communication Protocols from Source Code 
\item Michael Smith (University of Edinburgh, UK) 
\item PEPA Queues: Capturing customer behaviour in queueing networks 
\item Ashok Argent-Katwala and Jeremy Bradley (Imperial College London, UK) 
\item A structural approach for modelling performance of systems using skeletons 
\item Gagarine Yaikhom, Murray Cole, Stephen Gilmore and Jane Hillston (University of Edinburgh, UK) 

\end{description}
\subsubsection*{16:00 - 16:30 Coffee Break}
\subsubsection*{16:30 - 17:30 SESSION 4}
\begin{description}
\item[Short Paper Presentations: ]\item Distributed Liveness and Timers for Mobile Processes 
\item Martin Berger and Nobuko Yoshida (Imperial College London, UK) 
\item Stochastic Ambient Logic 
\item Maria Grazia Vigliotti (Imperial College London, UK) 

\end{description}
\subsubsection*{17:30 Steering Committee Meeting}
\subsubsection*{18:45 SOCIAL EVENT}
\begin{description}
\item[Joint Workshops Pre-Conference Dinner ]\item Dinner at Bom Jesus \emph{(Shutle departure from Campus Gualtar)}
 

\end{description}
\\ 
\subsubsection*{Further ETAPS 2007 Programme Information:}
\begin{itemize}
\item Programme Overview
\item Main Conferences: Complete Programme, CC, ESOP, FASE, FOSSACS, TACAS 
\item Workshops: ACCAT, Bytecode, COCV, FESCA, FinCo, GT-VMT, HAV, HFL, LDTA, MBT, MOMPES, OpenCert,  SC, SLA++P, TERMGRAPH, WITS, 
\item Tutorials: Stratego/XT, SoftwGen Mobius 
 
\end{itemize}
ETAPS 2007 | Top | HTML 4.01 | Last Update: 2007-03-13  \subsection{Programme of SC at ETAPS 2007}
\subsubsection{(Workshop on Software Composition)}
\subsubsection{Saturday, March 24, room: CP2-101}
\subsubsection*{09:00 - 10:30 SESSION 1}
\begin{description}
\item[Welcome ]\item[Invited Talk ]\item Composition by Anonymous Third Parties 
\item Farhad Arbab (CWI and Leiden University, NL) 

\end{description}
\subsubsection*{10:30 - 11:00 Coffee Break}
\subsubsection*{11:00 - 12:30 SESSION 2}
\begin{description}
\item[Composition Contracts ]\item Defining Component Protocols with Service Composition: Illustration with the Kmelia Model 
\item Pascal Andr\'e, Gilles Ardourel, and Christian Attiogb\'e (University Of Nantes, F) 
\item Composite Contract Enforcement in Hierarchical Component Systems 
\item Philippe Collet (University of Nice, F), Jacques Malenfant (University Paris 6, F), Alain Ozanne, and Nicolas Rivierre (France Telecom R\&D, F) 
\item Towards a Unifying Theory for Choreography Conformance and Contract Compliance 
\item Mario Bravetti and Gianluigi Zavattaro (University of Bologna, I) 

\end{description}
\subsubsection*{12:30 - 14:00 Lunch}
\subsubsection*{14:00 - 16:00 SESSION 3}
\begin{description}
\item[Composition Design \& Analysis ]\item A Process-Algebraic Approach to Workflow Specification and Refinement 
\item Peter Wong and Jeremy Gibbons (University of Oxford, UK) 
\item Generic Feature-Based Software Composition 
\item Tijs Van der Storm (CWI, NL) 
\item Composition Management Interfaces for a predictable assembly 
\item Xabier Aretxandieta, Goiuria Sagardui (University of Mondragon, E), and Franck Barbier (Pau University, F)\} 
\item Error propagation analysis in composition of software services 
\item Vittorio Cortellessa (Universita' dell'Aquila, I) and Pasqualina Potena (Universit\'a ``G. D'Annunzio'', I) 

\end{description}
\subsubsection*{16:00 - 16:30 Coffee Break}
\subsubsection*{16:30 - 18:00 SESSION 4}
\begin{description}
\item[Dynamic Composition ]\item Dynamically Adaptable Applications with iPOJO Service Components 
\item Clement Escoffier and Richard Hall (Grenoble University, F) 
\item Dynamic Contextual Service Ranking 
\item Andre Bottaro (France Telecom, F) and Richard Hall (Grenoble University, F) 
\item A Rapid Adaptive Algorithm for Finding Replacement Service Locally during Dynamic Service Composition 
\item Xingzhi Feng, Quanyuan Wu, Yan Jia, Bin Zhou, and Yi Ren (National University of Defense Technology, China) 

\end{description}
\\ 
\\ 
\subsubsection{Sunday, March 25, room: CP2-101}
\\ 
\subsubsection*{09:30 - 10:30 SESSION 1}
\begin{description}
\item[Short Papers ]\item Measuring Reactability of Persistent Computing Systems 
\item Takumi Endo, Yuichi Goto, and Jingde Cheng (Saitama University, Japan) 
\item Requirements for applying aspect-oriented techniques in webservice composition languages 
\item Mathieu Braem and Niels Joncheere (Vrije Universiteit Brussel, B) 
\item Synthesizing Communication Middleware from Explicit Connectors in Component Based Distributed Architectures 
\item Dietmar Schreiner and Karl G\"oschka (Vienna University of Technology, A) 
\item Streamlining Feature-Oriented Designs 
\item Martin Kuhlemann, Sven Apel, and Thomas Leich (University of Magdeburg, D) 
\item Requirements for Reusable Aspect Deployment 
\item Bruno De Fraine and Mathieu Braem (Vrije Universiteit Brussel, B) 

\end{description}
\subsubsection*{10:30 - 11:00 Coffee Break}
\subsubsection*{11:00 - 12:30 SESSION 2}
\begin{description}
\item[Aspect-Oriented Programming ]\item Aspect-Oriented Programming: Selecting and Exposing Object Paths 
\item Mohammed Al-Mansari, Stefan Hanenberg, and Rainer Unland (University of Duisburg-Essen, D) 
\item Debugging Aspect-Enabled Programs 
\item Marc Eaddy, Alfred Aho (Columbia University, USA), Weiping Hu, Paddy McDonald, and Julian Burger (Microsoft Corporation, USA) 
\item Unification of Static and Dynamic AOP for Evolution in Embedded Software Systems 
\item Wasif Gilani and Fabian Scheler (Erlangen University, D) 

\end{description}
\subsubsection*{12:30 - 14:00 Lunch}
\subsubsection*{14:00 - 16:00 SESSION 3}
\begin{description}
\item[Structural Composition ]\item Patterns of Component Evolution 
\item Rajesh Vasa (Swinburne University of Technology, AUS), Markus Lumpe (Iowa State University, USA), and Jean-Guy Schneider (Swinburne University of Technology, AUS) 
\item An Approach for Structural Pattern Composition 
\item Imed Hammouda and Kai Koskimies (Tampere University of Technology, FI) 
\item Composite Connectors for Composing Software Components 
\item Kung-Kiu Lau, Ling Ling, Vladyslav Ukis, and Perla Velasco (The University of Manchester, UK) 

\end{description}
\subsubsection*{16:00 - 16:30 Coffee Break}
\subsubsection*{16:30 - 17:00 SESSION 4}
\begin{description}
\item[Concluding Discussion and Remarks ]
\end{description}
\subsubsection*{18:45 SOCIAL EVENT}
\begin{description}
\item[Joint Workshops Pre-Conference Dinner ]\item Dinner at Bom Jesus \emph{(Shutle departure from Campus Gualtar)}
 

\end{description}
\\ 
\subsubsection*{Further ETAPS 2007 Programme Information:}
\begin{itemize}
\item Programme Overview
\item Main Conferences: Complete Programme, CC, ESOP, FASE, FOSSACS, TACAS 
\item Workshops: ACCAT, Bytecode, COCV, FESCA, FinCo, GT-VMT, HAV, HFL, LDTA, MBT, MOMPES, OpenCert, QAPL,  SLA++P, TERMGRAPH, WITS, 
\item Tutorials: Stratego/XT, SoftwGen Mobius 
 
\end{itemize}
ETAPS 2007 | Top | HTML 4.01 | Last Update: 2007-03-13  \subsection{Programme of SLA++P at ETAPS 2007}
\subsubsection{(Model-driven High-level Programming of Embedded Systems)}
\subsubsection{Saturday, March 31, room: CP2-105}
\subsubsection*{09:00 - 10:30 SESSION 1}
\begin{description}
\item Welcome and Opening 
\item (Invited Talk) 
\item Dr. Steven Miller, Senior Principal Engineer in the Advanced Technology Center of Rockwell Collins, USA 
\item A Model Checking Approach to Protocol Conversion 
\item R.Sinha, P.S.Roop, S.Basu 

\end{description}
\subsubsection*{10:30 - 11:00 Coffee Break}
\subsubsection*{11:00 - 12:30 SESSION 2}
\begin{description}
\item Worst Case Reaction Time Analysis of Concurrent Reactive Programs 
\item M.Boldt, C.Traulsen, R.von Hanxleden 
\item Executable Specifications for Real-Time Distributed Systems 
\item A.Ray, R.Cleaveland 
\item (Short discussion) SYNCHRON'07 and SLAP'08 

\end{description}
\subsubsection*{12:30 - 14:00 Lunch}
\subsubsection*{14:00 - 15:30 SESSION 3}
\begin{description}
\item Gotos in Esterel 
\item O.Tardieu, S.A.Edwards 
\item Specifying and executing reactive scenarios with Lutin 
\item P.Raymond, Y.Roux, E.Jahier 
\item Modifying Contracts with Larissa Aspects 
\item D.Stauch 

\end{description}
\subsubsection*{15:30 - 16:00 Coffee Break}
\subsubsection*{16:00 - 18:30 SESSION 4}
\begin{description}
\item Lustre as a System Modeling Language: Lussensor, a Case-Study with Sensor Networks 
\item F.Maraninchi, L.Samper, K.Baradon, A.Vasseur Madrid, Spain 
\item Mutation analysis for LUSTRE programs 
\item L.du Bousquet 
\item Extending Lustre with Timeout Automata 
\item J.Gao, M.Whalen, E.Van Wyk 

\end{description}
\subsubsection*{18:45 SOCIAL EVENT}
\begin{description}
\item[Joint Workshops Post-Conference Dinner ]\item Dinner at Pousada Santa Maria de Bouro \emph{(Shutle departure from Campus Gualtar)}
 

\end{description}
\\ 
\subsubsection*{Further ETAPS 2007 Programme Information:}
\begin{itemize}
\item Programme Overview
\item Main Conferences: Complete Programme, CC, ESOP, FASE, FOSSACS, TACAS 
\item Workshops: ACCAT, Bytecode, COCV, FESCA, FinCo, GT-VMT, HAV, HFL, LDTA, MBT, MOMPES, OpenCert, QAPL, SC,  TERMGRAPH, WITS, 
\item Tutorials: Stratego/XT, SoftwGen Mobius 
 
\end{itemize}
ETAPS 2007 | Top | HTML 4.01 | Last Update: 2007-03-13  \subsection{Programme of Termgraph at ETAPS 2007}
\subsubsection{(4th International Workshop on Computing with Terms and Graphs)}
\subsubsection{Saturday, March 31, room: CP2-104}
\subsubsection*{09:20 - 10:30 SESSION 1}
\begin{description}
\item Welcome 
\item An Algebra for Directed Bigraphs 
\item D. Grohmann and M. Miculan 
\item Modeling and Verifying Graph Transformations in Proof Assistants 
\item M. Strecker 

\end{description}
\subsubsection*{10:30 - 11:00 Coffee Break}
\subsubsection*{11:00 - 12:30 SESSION 2}
\begin{description}
\item Intensional properties of polygraphs 
\item G. Bonfante and Y. Guiraud 
\item Term-graph rewriting in TOM with relative positions 
\item E. Balland and P. Brauner 
\item Deduction Graphs with Universal Quantification 
\item H. Geuvers and I. Loeb 

\end{description}
\subsubsection*{12:30 - 14:00 Lunch}
\subsubsection*{14:00 - 16:00 SESSION 3}
\begin{description}
\item Rewritings for Polarized Mutiplicative and Exponential Proof Structures 
\item C. Fouquere and V. Mogbil 
\item Hard Combinators 
\item D. Bechet and S. Lippi 
\item Universal Boolean Systems 
\item D. Bechet and S. Lippi 
\item Interaction Nets with Nested Pattern Matching 
\item S. Sato and A. Hussan 
\item Sub-lambda-calculi, classified 
\item F-R. Sinot 

\end{description}
\subsubsection*{16:00 - 16:30 Coffee Break}
\subsubsection*{18:45 SOCIAL EVENT}
\begin{description}
\item[Joint Workshops Post-Conference Dinner ]\item Dinner at Pousada Santa Maria de Bouro \emph{(Shutle departure from Campus Gualtar)}
 

\end{description}
\\ 
\subsubsection*{Further ETAPS 2007 Programme Information:}
\begin{itemize}
\item Programme Overview
\item Main Conferences: Complete Programme, CC, ESOP, FASE, FOSSACS, TACAS 
\item Workshops: ACCAT, Bytecode, COCV, FESCA, FinCo, GT-VMT, HAV, HFL, LDTA, MBT, MOMPES, OpenCert, QAPL, SC, SLA++P,  WITS, 
\item Tutorials: Stratego/XT, SoftwGen Mobius 
 
\end{itemize}
ETAPS 2007 | Top | HTML 4.01 | Last Update: 2007-03-13  \subsection{Programme of WITS at ETAPS 2007}
\subsubsection{(7th International Workshop on Issues in the Theory of Security)}
\subsubsection{Saturday, March 24, room: CP2-102}
\subsubsection*{09:00 - 10:30 SESSION 1}
\begin{description}
\item[Welcome ]\item Riccardo Focardi (University of Venice) 
\item[Invited Talk ]\item On the use of formal models for proving cryptographic security notions 
\item V\'eronique Cortier 

\end{description}
\subsubsection*{10:30 - 11:00 Coffee Break}
\subsubsection*{11:00 - 12:30 SESSION 2}
\begin{description}
\item[Computational Security ]\item Computationally Sound Analysis of Protocols using Bilinear Pairings 
\item Laurent Mazare 
\item On the Role of Scheduling in Simulation-Based Security 
\item Ran Canetti, Ling Cheung, Nancy Lynch and Olivier Pereira 
\item Inductive Trace Properties Imply Computational Security 
\item Arnab Roy, Anupam Datta, Ante Derek and John Mitchell 

\end{description}
\subsubsection*{12:30 - 14:00 Lunch}
\subsubsection*{15:00 - 16:00 SESSION 3}
\begin{description}
\item[Information Flow ]\item On information flow and refinement-closure 
\item Gavin Lowe 
\item Nondeduciblity on strategies in the temporal logic of knowledge 
\item Catalin Dima and Constantin Enea 

\end{description}
\subsubsection*{16:00 - 16:30 Coffee Break}
\subsubsection*{16:30 - 17:30 SESSION 4}
\begin{description}
\item[Static Analysis of Authentication ]\item Detecting Replay Attacks by Freshness Annotations 
\item Han Gao, Pierpaolo Degano, Chiara Bodei and Hanne Riis Nielson 
\item A Calculus of Challanges and Responses 
\item Michael Backes, Agostino Cortesi, Riccardo Focardi and Matteo Maffei 

\end{description}
\\ 
\\ 
\subsubsection{Sunday, March 25, room: CP2-102}
\\ 
\subsubsection*{09:30 - 10:30 SESSION 1}
\begin{description}
\item[Invited Talk ]\item Certified access control on mobile interactive devices 
\item Thomas Jensen (Saitama University, Japan) 

\end{description}
\subsubsection*{10:30 - 11:00 Coffee Break}
\subsubsection*{11:00 - 12:30 SESSION 2}
\begin{description}
\item[New Models for Security Protocols ]\item On the Specification of Secure Channels 
\item Christopher Dilloway and Gavin Lowe 
\item Causality-based Abstraction of Multiplicity in Security Protocols 
\item Michael Backes, Agostino Cortesi and Matteo Maffei 
\item Skeletons and the Shapes of Bundles 
\item Joshua Guttman, Shaddin Doghmi and F. Javier Thayer 

\end{description}
\subsubsection*{12:30 - 14:00 Lunch}
\subsubsection*{15:00 - 16:00 SESSION 3}
\begin{description}
\item[Protocol Verification ]\item Verifying an implementation of SSH 
\item Erik Poll and Aleksy Schubert 
\item Partial Order Reduction for Branching Security Protocols 
\item Wan Fokkink, Mohammad Torabi Dashti and Anton Wijs 

\end{description}
\subsubsection*{16:00 - 16:30 Coffee Break}
\subsubsection*{16:30 - 17:30 IFIP WG 1.7 Business Meeting}
\subsubsection*{18:45 SOCIAL EVENT}
\begin{description}
\item[Joint Workshops Pre-Conference Dinner ]\item Dinner at Bom Jesus \emph{(Shutle departure from Campus Gualtar)}
 

\end{description}
\\ 
\subsubsection*{Further ETAPS 2007 Programme Information:}
\begin{itemize}
\item Programme Overview
\item Main Conferences: Complete Programme, CC, ESOP, FASE, FOSSACS, TACAS 
\item Workshops: ACCAT, Bytecode, COCV, FESCA, FinCo, GT-VMT, HAV, HFL, LDTA, MBT, MOMPES, OpenCert, QAPL, SC, SLA++P, TERMGRAPH,  
\item Tutorials: Stratego/XT, SoftwGen Mobius 
 
\end{itemize}
ETAPS 2007 | Top | HTML 4.01 | Last Update: 2007-03-13  \section{Tutorials}
\\ 
\begin{itemize}
\item \textbf{Program Transformation with Stratego/XT}
, 
\item \textbf{Beyond the Generators: Practical Techniques for Real-World Software Generation}
 
\item \textbf{Mobility, Ubiquity, and Security}
 
 
\end{itemize}
\\ 
\\ 
\subsubsection{Program Transformation with Stratego/XT}


 \textbf{Saturday, March 24, room: DI 1.09}
 


  This tutorial gives an overview of techniques for program transformation, illustrated through the Stratego/XT program transformation system. We explain the general architecture of transformation systems, and how Stratego/XT is used to assemble such systems from components. We introduce a set of ready made components for Java transformation, and show how to program custom transformation components using Stratego. In particular, we show how to express local transformations using rewrite rules and strategies and how context-sensitive transformations can be expressed easily using dynamic rewrite rules. All techniques and language features are illustrated with implementations of transformations on Java programs, that show how to apply all introduced techniques in practice. 
\textbf{Speakers: }
\begin{itemize}
\item Martin Bravenboer (Utrecht University)
\item Eelco Visser (Delft University of Technology)
 
\end{itemize}
\subsubsection{Beyond the Generators: Practical Techniques for Real-World Software Generation}


 \textbf{Saturday, March 24, room: CP2 106}
 


  Most of the available literature on software generation concentrates on how to build generators that transform specifications into code. Little is said about the following important peripheral issues: 
\begin{itemize}
\item  justification: how to convince people that generation is worth it 
\item  debugging: how to understand what the generated code is doing 
\item  structuring: how to describe multi-language generator specifications 
\item  manufacturing: how to formally describe the generation process 

\end{itemize}


  This tutorial presents practical techniques for addressing these issues based on almost twenty years of experience with a complex, multi-language generation system. 
\textbf{Speakers: }
\begin{itemize}
\item Anthony M. Sloane (Macquarie University)
 
\end{itemize}
\subsubsection{Mobility, Ubiquity, and Security}


 \textbf{Sunday, April 1, root: CP2 103}
 


  The European project Mobius develops the technology for establishing trust and security for Java-enabled global computers such as mobile telephone networks. Mobius uses the Proof-Carrying Code (PCC) paradigm to provide static guarantees for security and functional properties of code. Certificates can be produced and checked using various enabling technologies such as advanced type systems and logic-based reasoning. This tutorial will introduce participants to both the central security architecture of Mobius as well as type systems, logics, and tools that enable static verification of Java source and bytecode. 
\textbf{Speakers: }
\begin{itemize}
\item Gilles Barthe (INRIA)
\item David Pichardie (IRISA)
\item David Aspinall (Univ. of Edinburgh)
\item Peter M\"uller (ETH Zurich)
\item Lennart Beringer (LMU Munich)
\item Joe Kiniry (UC Dublin)
 
\end{itemize}
\textbf{Brochure:}
 MobiusTutorial.pdf\\ 
\\ 


  
 
\section{Social Programme}

\section{All events day by day}

\section{Sponsors}



\end{document}