\documentclass[twoside,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{fancyhdr} \usepackage{t1enc} \usepackage{url} \usepackage{aeguill} \usepackage{graphicx} \usepackage{pdfpages} \usepackage{compact} %\def\sp{\mbox{}\hspace{8mm}} \def\sp{} \pagestyle{fancy} \fancyhead[LE,RO]{\small\thepage} \fancyfoot[R,L]{} %\fancyfoot[C]{\today} \fancyfoot[C]{} \renewcommand{\subsectionmark}[1]{\markboth{ \thesubsection.\ #1}{}} \renewcommand{\subsubsectionmark}[1]{\markright{ \thesubsubsection.\ #1}} %\rhead{\nouppercase{\rightmark}} %\lhead{\nouppercase{\leftmark}} \fancyhead[LO]{\nouppercase{\small\rightmark}} \fancyhead[RE]{\nouppercase{\small\leftmark}} %\fancyhead[RE,LO]{} \begin{document} \thispagestyle{empty} \includepdf[offset=0mm 3mm,scale=.94]{capa.pdf} %\mbox{}\hspace{-2cm}\includegraphics[width=1.15\textwidth]{capa.png} \thispagestyle{empty} \newpage \thispagestyle{empty} \parindent 0pt \parskip 0pt \subsection*{Steering Committee} Perdita Stevens (Edinburgh Chair) Roberto Amadio (Paris) Luciano Baresi (Milan) Sophia Drossopoulou (London) Matt Dwyer (Lincoln) Hartmut Ehrig (Berlin) José Fiadeiro (Leicester) Chris Hankin (London) Laurie Hendren (McGill) Mike Hinchey (NASA Goddard) Michael Huth (London) Anna Ingólfsdóttir (Aalborg) Paola Inverardi (L'Aquila) 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) Jakob Rehof (Dortmund) Don Sannella (Edinburgh) João Saraiva (Braga) Vladimiro Sassone (Southampton) Helmut Seidl (Munique) Dániel Varró (Budapest) Andreas Zeller (Saarbrücken) \subsection*{Organizing Committee} João Alexandre Saraiva (Chair) José Bacelar Almeida (Web site) José João Almeida (Publicity) Luis Soares Barbosa (Satellite events, Finances) Victor Francisco Fonte (Web site) Pedro Rangel Henriques (Local Arrangements) José Nuno Oliveira (Industrial Liaison) Jorge Sousa Pinto (Publicity) António Nestor Ribeiro (Fundraising) Joost Visser (Satellite events) \newpage \tableofcontents \newpage \parskip 4pt \section{Welcome} \subsection*{Welcome to ETAPS 2007} The European Joint Conferences on Theory and Practice of Software (ETAPS) are the primary European forum for academic and industrial researchers working on topics relating to Software Science. ETAPS, established in 1998, is a confederation of five main annual conferences, accompanied by satellite workshops and other events. ETAPS 2007 in Braga is the tenth event in the series, after Lisbon, Amsterdam, Berlin, Genova, Grenoble, Warsaw, Barcelona, Edinburgh, and Vienna. Over 9 days, ETAPS 2007 will offer 7 invited talks by distinguished speakers, 5 main conferences, 17 workshops, 3 tutorials, and a significant number of invited talks specific to the satellite events. Overall, the five main conferences received this year around 630 submitted papers, with an acceptance rate of 25\%. The high quality and quantity of the submitted papers required the overlapping of four conferences on Wednesday, for the first time in the history of ETAPS. ETAPS 2007 marks the tenth anniversary of the conference. To celebrate the event, brief talks will be given by some of those who have been involved in ETAPS over the years: Hartmut Ehrig, Reinhard Wilhelm, Don Sannella, José Fiadeiro, and Perdita Stevens. An informal panel will follow. \subsection*{Welcome to Braga} ETAPS 2007 will be held in Braga, an ancient city in the heart of the green and fertile region known as the Costa Verde in the North of Portugal. It is the capital of the Minho province, and formerly was (as Bracara Augusta) the capital of the Roman province of Gallaecia, and of the Suebic kingdom in Gallaecia. Braga, which is known for its baroque churches and splendid 18th century houses, is a modern, fast-growing commercial town. The old city, solemn and antique, is animated with academic and cultural life and with its characterful nineteenth-century cafés, a good choice of restaurants serving splendid traditional gastronomy, and a number of lively bars. \subsection{Conferences and Workshops Location} ETAPS 2007 will be held in Braga at two locations. The events from Monday 26th until Friday 30th March will take place in Theatro Circo, located in the city centre. The satellite events at the enclosing weekends (24th/25th and 31th March/1st April) will be held at the University's Campus of Gualtar, 2 Km east of the city centre. \subsubsection*{ETAPS Conferences at Theatro Circo} Theatro Circo, the main theater of Braga, is located in the city centre (see map below). The building, designed by the Portuguese architect Moura Coutinho, was built in 1914. Due to its architecture and size it is considered one of the largest and most beautiful theaters of Portugal. In 2004 and 2005, Theatro Circo underwent major renovation and extension. It now includes modern facilities to host music concerts, theatre plays, cinema, and conferences. \subsubsection*{ETAPS Satellite Events at Campus of Gualtar } Most of departmental and teaching buildings of Universidade do Minho are located in the Campus of Gualtar in Braga. Campus of Gualtar is located 2 km east of the city centre. The satellite events will be located in the building "Complexo Pedagógico 2" (CP 2, see map below). \subsubsection*{Registration Desk } The registration desk will be located: \begin{itemize} \item from March 26 till March 30 --- Entrance hall of Theatro Circo; opening hours: 8:30 - 18:00. \item on March 24, 25 and March 30, April 1 --- Entrance hall of the CP2 building at the Gualtar campus; opening hours: 8:30 - 18:00. \end{itemize} \subsubsection*{Lunch } Lunch is not included in the main conference registration fee. There are several restaurants located in the city centre of Braga that can be easily reached from Theatro Circo. Most of these restaurants serve a very affordable daily meal. On March 24, 25 and 30 and April 1, lunch is included in the workshops registration fee. The workshop lunches will be served in the University restaurant located in the Campus of Gualtar. The workshop daily fee covers the participants' lunches and coffee-breaks. \subsection*{Shuttle Service} A shuttle service will be run during ETAPS. On weekends, shuttles will leave towards the university campus at Gualtar, from the following places: \begin{itemize} \item Train station (S1 in the map, close to the WS Braga SPRU -- Student Residence and Hotel da Estação) \item Hotel Turismo (S2 in the map, close to all hotels in the city centre) \item Bom Jesus (Hotel do Elevador) \end{itemize} On weekdays, the shuttle service will run from Bom Jesus only, towards the main conference venue (Theatro Circo). An organisation representative will be present at each shuttle departure time. The shuttle timetable is as follows: \begin{description} \item [Friday (23/03)]\ \begin{itemize} \item 8:30: Hotel Turismo $\longrightarrow$ Campus of Gualtar \item 18:30: Campus of Gualtar $\longrightarrow$ city centre \end{itemize} \item [Saturday (24/03)]\ \begin{itemize} \item 8:15: Train Station $\longrightarrow$ Campus of Gualtar \item 8:15: Hotel Turismo $\longrightarrow$ Campus of Gualtar \item 8:15: Bom Jesus $\longrightarrow$ Campus of Gualtar \item 18:45: Campus of Gualtar $\longrightarrow$ city centre \end{itemize} \item [Sunday (25/03)]\ \begin{itemize} \item 8:15: Train Station $\longrightarrow$ Campus of Gualtar \item 8:15: Hotel Turismo $\longrightarrow$ Campus of Gualtar \item 8:15: Bom Jesus $\longrightarrow$ Campus of Gualtar \item 18:45: Campus of Gualtar $\longrightarrow$ city centre \item 18:45: Campus of Gualtar $\longrightarrow$ Bom Jesus (dinner) \item 23:00: Bom Jesus $\longrightarrow$ city centre \end{itemize} \item [Monday (26/03)]\ \begin{itemize} \item 8:15: Bom Jesus $\longrightarrow$ Teatro Circo \item 22:00: Teatro Circo $\longrightarrow$ Bom Jesus \end{itemize} \item [Tuesday (27/03)]\ \begin{itemize} \item 8:15: Bom Jesus $\longrightarrow$ Teatro Circo \item 23:00: Teatro Circo $\longrightarrow$ Bom Jesus \end{itemize} \item [Wednesday (28/03)]\ \begin{itemize} \item 8:15: Bom Jesus $\longrightarrow$ Teatro Circo \item 19:00: Teatro Circo $\longrightarrow$ Banquete \end{itemize} \item [Thursday (29/03)]\ \begin{itemize} \item 8:15: Bom Jesus $\longrightarrow$ Teatro Circo \item 22:00: Teatro Circo $\longrightarrow$ Bom Jesus \end{itemize} \item [Friday (30/03)]\ \begin{itemize} \item 8:15: Bom Jesus $\longrightarrow$ Teatro Circo \item 22:00: Teatro Circo $\longrightarrow$ Bom Jesus \end{itemize} \item [Saturday (31/03)]\ \begin{itemize} \item 8:15: Train Station $\longrightarrow$ Campus of Gualtar \item 8:15: Hotel Turismo $\longrightarrow$ Campus of Gualtar \item 8:15: Bom Jesus $\longrightarrow$ Campus of Gualtar \item 18:45: Campus of Gualtar $\longrightarrow$ city centre \item 18:45: Campus of Gualtar $\longrightarrow$ Pousada Bouro (dinner) \end{itemize} \item [Sunday (01/04)]\ \begin{itemize} \item 8:15: Hotel Turismo $\longrightarrow$ Campus of Gualtar \item 18:45: Campus of Gualtar $\longrightarrow$ city centre \end{itemize} \end{description} \newpage \thispagestyle{empty} \includegraphics[width=\textwidth]{mapa-gualtar.png} \newpage \thispagestyle{empty} \mbox{} \hspace{1.7cm} \includegraphics[height=22.5cm]{bragaleft.png} \newpage \thispagestyle{empty} \mbox{} \hspace{-1.5cm} \includegraphics[height=22.5cm]{bragaright.png}\\ \includegraphics[height=1.8cm]{legenda.png} \newpage \section{Main Conferences} \subsection{Conference Description} \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} \subsubsection*{CC 2007: 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} \textbf{Invited Speaker:} Don Batory, University of Texas at Austin \textbf{URL: } \url{http://cc2007.cs.brown.edu/} \subsubsection*{ESOP 2007: 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} \textbf{Invited Speaker:} Andrew Pitts - Cambridge University, UK \textbf{URL: } \url{http://rap.dsi.unifi.it/esop07/} \subsubsection*{FASE 2007: 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} \textbf{Invited Speaker:} Jan Bosch (Nokia, Finland) \textbf{URL: } \url{http://fase07.di.fc.ul.pt} \subsubsection*{FOSSACS 2007: 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} \textbf{Invited Speaker:} Radha Jagadeesan, DePaul University \textbf{URL: } \url{http://www2.in.tum.de/~seidl/fossacs07/} \subsubsection*{TACAS 2007: 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{itemize} \item Christel Baier -- Universit\"at Bonn, Bonn (Germany) \item Armin Biere -- Johannes Kepler Universit\"at, Linz (Austria) \item Jonathan Billington -- University of South Australia, Mawson Lakes (Australia) \item Ed Brinksma -- ESI and University of Twente (The Netherlands) \item Rance Cleaveland -- University of Maryland \& Fraunhofer USA Inc, College Park, Maryland (USA) \item Byron Cook (tool chair) -- Microsoft Research, Cambridge (UK) \item Dennis Dams -- Lucent Technologies, Murray Hill, New Jersey (USA) \item Marsha Chechik -- University of Toronto, Toronto (Canada) \item Francois Fages -- INRIA Rocquencourt, Le Chesnay Cedex (France) \item Kathi Fisler -- Worcester Polytechnic Institute, Worcester, Massachusetts (USA) \item Limor Fix -- Intel Research Laboratory at Pittsburgh, Pittsburgh, Pennsylvania (USA) \item Hubert Garavel -- INRIA Rhones-Alpes, Montbonnot Saint-Martin (France) \item Susanne Graf -- VERIMAG, Grenoble - Gi\`eres (France) \item Orna Grumberg (co-chair) -- TECHNION - Israel Institute of Technology, Haifa (Israel) \item John Hatcliff -- Kansas State University, Manhattan, Kansas (USA) \item Holger Hermanns -- Universit\"at des Saarlandes, Saarbruecken (Germany) \item Michael Huth (co-chair) -- Imperial College London, London (UK) \item Daniel Jackson -- Massachusetts Institute of Technology, Cambridge, Massachusetts (USA) \item Somesh Jha -- The University of Wisconsin at Madison, Madison, Wisconsin (USA) \item Orna Kupferman -- Hebrew University, Jerusalem (Israel) \item Marta Kwiatkowska -- University of Birmingham, Birmingham, England (UK) \item Kim Larsen -- Aalborg University, Aalborg (Denmark) \item Michael Leuschel -- Heinrich-Heine-Universit\"at D\"usseldorf, D\"usseldorf (Germany) \item Andreas Podelski -- Max-Planck-Institut f\"ur Informatik, Saarbr\"ucken (Germany) \item Tiziana Margaria-Steffen -- Universit\"at Potsdam, Potsdam (Germany) \item Tom Melham -- Oxford University, Oxford (UK) \item Natarajan Shankar -- SRI, Menlo Park, California (USA) \item Bernhard Steffen -- Universit\"at Dortmund, Dortmund (Germany) \item Lenore Zuck -- University of Illinois, Chicago, Illinois (USA) \end{itemize} \textbf{Invited Speaker:} K. Rustan M. Leino (Microsoft Research, USA) \textbf{URL: } \url{http://www.doc.ic.ac.uk/tacas07/} \newpage \subsection{Main Conference Programmes} \subsubsection{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) ]\ \begin{itemize} \item New Algorithms for SIMD Alignment \\ \sp 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 \\ \sp 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 \\ \sp K. Shyam, R. Govindarajan (Indian Institute of Science) \end{itemize} \item[FOSSACS - Games and Mu Calculus (Chair: Helmut Seidl) ]\ \begin{itemize} \item Optimal Strategy Synthesis in Stochastic M\"uller Games \\ \sp Krishnendu Chatterjee (Univ. of California, Berkeley) \item Generalized Parity Games \\ \sp Nir Piterman (EPFL Switzerland), Krishnendu Chatterjee (Univ. of Califonria, Berkeley), Thomas A. Henzinger (EPFL Switzerland) \item Enriched mu-Calculi Module Checking \\ \sp Aniello Murano (Univ. di Napoli), Alessandro Ferrante (Univ. di Salerno) \end{itemize} \item[TACAS - Software Verification (Chair: Natasha Sharygina) ] \ \begin{itemize} \item Shape Analysis by Graph Decomposition \\ \sp 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 \\ \sp 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 \\ \sp Muhammad Zubair Malik, Aman Pervaiz, and Sarfraz Khurshid (University of Texas at Austin) \end{itemize} \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) ]\ \begin{itemize} \item Using Prefetching to Improve Reference-Counting Garbage Collectors \\ \sp Harel Paz (IBM Haifa Research Laboratory), Erez Petrank (Microsoft Research) \item Accurate Garbage Collection in Uncooperative Environments with Lazy Pointer Stacks \\ \sp Jason Baker, Antonio Cunei, Filip Pizlo, Jan Vitek (Purdue University) \item Correcting the Dynamic Call Graph Using Control-Flow Constraints \\ \sp 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 \\ \sp Michael Batchelder, Laurie Hendren (McGill University) \end{itemize} \item[FOSSACS - Logic (Chair: Hubert Comon) ]\ \begin{itemize} \item The Complexity of Generalized Satisfiability for Linear Temporal Logic \\ \sp 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 \\ \sp Markus Lohrey (Univ. Stuttgart), Carsten Lutz (TU Dresden), Stefan G\"oller (Univ. Stuttgart) \item On the Expressiveness and Complexity of ATL \\ \sp Nicolas Markey (ENS Cachan), Ghassan Oreiby (ENS Cachan), Francois Laroussinie (ENS Cachan) \item Formalising the pi-calculus using Nominal Logic \\ \sp Jesper Bengtson (Uppsala Univ.), Joachim Parrow (Uppsala Univ.) \end{itemize} \item[TACAS - Probabilistic Model Checking and Markov Chains (Chair: Holger Hermanns) ]\ \begin{itemize} \item Multi-Objective Model Checking of Markov Decision Processes \\ \sp 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 \\ \sp Dominik Wojtczak and Kousha Etessami (University of Edinburgh) \item Counterexamples in Probabilistic Model Checking \\ \sp Tingting Han and Joost-Pieter Katoen (RWTH Aachen and University of Twente) \item Bisimulation minimisation mostly speeds up probabilistic model checking \\ \sp 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{itemize} \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) ]\ \begin{itemize} \item A Fast Cutting-Plane Algorithm for Optimal Coalescing \\ \sp 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 \\ \sp Santosh G. Nagarakatte, R. Govindarajan (Indian Institute of Science) \item Extended Linear Scan: an Alternate Foundation for Global Register Allocation \\ \sp Vivek Sarkar (IBM T.J. Watson Research Center), Rajkishore Barik (IBM India Research Laboratory) \end{itemize} \item[FOSSACS - Formal Languages and Complexity (Chair: Igor Walukiewicz) ]\ \begin{itemize} \item Symbolic Reachability Analysis for Higher-Order Pushdown Systems \\ \sp Matthew Hague (Oxford Univ.), Luke Ong (Oxford Univ.) \item Complexity Results on Balanced Context-Free Languages \\ \sp Akihiko Tozawa (IBM Research, Tokyo), Yasuhiko Minamide (Univ. of Tsukuba) \item An Effective Algorithm for The Membership Problem for Extended Regular Expressions \\ \sp Grigore Rosu (Univ. of Illinois, Urbana) \end{itemize} \item[TACAS - Static Analysis (Chair: Tiziana Margaria) ]\ \begin{itemize} \item Causal Concurrent Dataflow Analysis for Concurrent Programs \\ \sp Azadeh Farzan and P. Madhusudan (University of Illinois at Urbana-Champaign) \item Type-dependency Analysis and Program Transformation for Symbolic Execution \\ \sp Saswat Anand, Alessandro Orso, and Mary Jean Harrold (Georgia Institute of Technology) \item JPF--SE: A Symbolic Execution Extension to Java PathFinder \\ \sp Saswat Anand (Georgia Institute of Technology), Corina S. Pasareanu, and Willem Visser (NASA Ames Research Center) \end{itemize} \end{description} \subsubsection*{19:00 SOCIAL EVENT (Monday)} \begin{description} \item[Welcome Reception (free admittance) ]\ \item Largo do Pa\c{c}o (\emph{University Rectorate Building} ) \item The \emph{Etaps Organization} invites all ETAPS participants to the welcome reception \end{description} \newpage \subsubsection{Tuesday, March 27} \subsubsection*{09:00 - 10:00 SESSION 1 (Tuesday)} \begin{description} \item[CC - Invited Talk (Chair: Shriram Krishnamurthi) ]\ \begin{itemize} \item On the Convergence of Program Refactoring, Program Synthesis, and Model Driven Development \\ \sp Don Batory (U. Austin, USA) \end{itemize} \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) ]\ \begin{itemize} \item A Practical Escape and Effect Analysis for Building Lightweight Method Summaries \\ \sp Sigmund Cherem, Radu Rugina (Cornell University) \item Layout Transformations for Heap Objects Using Static Access Patterns \\ \sp Jinseong Jeon, Keoncheol Shin, Hwansoo Han (Korea Advanced Institute of Science and Technology) \item A New Elimination-Based Data Flow Analysis Framework \\ \sp Bernhard Scholz (University of Sydney), Johann Blieberger (Technische Universit$\backslash$''at Wien) \item A declarative framework for analysis and optimization components \\ \sp Henry Falconer, Paul H. J. Kelly, David M. Ingram, Michael R. Mellor, Tony Field, Olav Beckmann (Imperial College) \end{itemize} \item[FOSSACS - Process Calculi (Chair: Pierpaolo Degano) ]\ \begin{itemize} \item A Distribution Law for CCS and a New Congruence Result for the Pi-calculus \\ \sp Daniel Hirschkoff (ENS Lyon), Damien Pous (ENS Lyon) \item Semantic barbs and biorthogonality \\ \sp Pawel Sobocinski (Univ. of Cambridge), Vladimiro Sassone (Univ. of Southampton), Julian Rathke (Univ. of Sussex) \item Logical Characterizations of Bisimulations for Discrete Probabilistic Systems \\ \sp Augusto Parma (Univ. di Verona), Roberto Segala (Univ. di Verona) \item Approximating a Behavioural Pseudometric without Discount for Probabilistic Systems \\ \sp Franck van Breugel (York Univ.), James Worrell (Oxford Univ.), Babita Sharma (York Univ.) \end{itemize} \item[TACAS - Markov Chains and Real-Time Systems (Chair: Joost-Pieter Katoen) ]\ \begin{itemize} \item A Symbolic Algorithm for Optimal Markov Chain Lumping \\ \sp Salem Derisavi (Carleton University at Ottawa) \item Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations \\ \sp 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 \\ \sp Marcin Jurdzinski (University of Warwick), Francois Laroussinie (ENS Cachan), and Jeremy Sproston (Universita di Torino) \item Adaptor synthesis for real-time components \\ \sp Massimo Tivoli (University of L'Aquila), Pascal Fradet, Alain Girault, Gregor Goessler (INRIA Rhone-Alpes) \end{itemize} \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) ]\ \begin{itemize} \item Logical Reasoning for Higher-Order Functions with Local State \\ \sp Nobuko Yoshida (Imperial College London), Kohei Honda (Queen Mary), and Martin Berger (Imperial College London) \item Types and Effects for Resource Usage Analysis \\ \sp 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 \\ \sp Hongseok Yang (Univ. of London), Lars Birkedal (IT Univ. of Copenhagen) \item Polynomial Constraints for Sets with Cardinality Bounds \\ \sp Bruno Marnette (ENS Cachan), Martin Rinard (MIT, Cambridge, USA), Viktor Kuncak (MIT, Cambridge, USA) \end{itemize} \item[TACAS (I) - Timed Automata and Duration Calculus (Chair: Joel Ouaknine) ]\ \begin{itemize} \item Deciding an Interval Logic with Accumulated Durations \\ \sp Martin Fraenzle (Universitat Oldenburg) and Michael R. Hansen (Technical University of Denmark) \item From Time Petri Nets to Timed Automata: an Untimed Approach \\ \sp 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 \\ \sp Jacob Illum Rasmussen, Gerd Behrmann, and Kim G. Larsen (Aalborg University) \item On Sampling Abstraction of Continuous Time Logic with Durations \\ \sp Paritosh K. Pandya (Tata Institute of Fundamental Research), Shankara Narayanan Krishna, and Kuntal Loya (Indian Institute of Technology at Bombay) \end{itemize} \item[TACAS (II) - Assume-Guarantee Reasoning (Chair: Moshe Vardi) ]\ \begin{itemize} \item Assume Guarantee Synthesis \\ \sp Krishnendu Chatterjee (University of California, Berkeley) and Thomas A. Henzinger (EPFL) \item Optimized L* for Assume-Guarantee Reasoning \\ \sp Sagar Chaki (Software Engineering Institute) and Ofer Strichman (The Technion, Haifa) \item Refining Interface Alphabets for Compositional Verification \\ \sp Mihaela Gheorghiu (University of Toronto), Dimitra Giannakopoulou, and Corina S. Pasareanu NASA Ames Research Center) \item MAVEN: Modular Aspect Verification \\ \sp Max Goldman and Shmuel Katz (The Technion, Haifa) \end{itemize} \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) ]\ \begin{itemize} \item EQ-Mine: Predicting Short-Term Defects for Software Evolution \\ \sp 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 \\ \sp 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 \\ \sp Paulo Salem da Silva (University of S\~ao Paulo, Brazil), Ana C. V. de Melo (University of S\~ao Paulo, Brazil) \end{itemize} \item[FOSSACS - Calculi (Chair: Antoine Mine) ]\ \begin{itemize} \item The Rewriting Calculus as a Combinatory Reduction System \\ \sp Clara Bertolissi (Univ. de Provence), Claude Kirchner (INRIA/LORIA, Nancy) \item Iterator Types \\ \sp 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 \\ \sp Colin Riba (INPL/LORIA, Nancy) \end{itemize} \item[TACAS - Biological Systems (Chair: Radha Jagadeesan) ]\ \begin{itemize} \item Model Checking Liveness Properties of Genetic Regulatory Networks \\ \sp Gregory Batt and Calin Belta (Boston University), and Ron Weiss (Princeton University) \item Checking Pedigree Consistency with SAT \\ \sp 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 \\ \sp 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{itemize} \end{description} \subsubsection*{19:00 SOCIAL EVENT (Tuesday)} \begin{description} \item[10th Anniversary Celebration (free admittance) ]\item \emph{Theatro Circo} \item Cocktail/Buffet \item Panel on the \emph{History of ETAPS} \item Anniversary Cake + Port Wine + Fado Concert \end{description} \newpage \subsubsection{Wednesday, March 28} \subsubsection*{09:00 - 10:10 SESSION 1 (Wednesday)} \begin{description} \item[Unifying Invited Talk (Chair: Perdita Stevens) ]\ \begin{itemize} \item There and Back Again: Lessons Learned on the Way to the Market \\ \sp Rance Cleaveland (University of Maryland/Fraunhofer USA Center for Experimental Software Engineering and Reactive Systems Inc., USA) \end{itemize} \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) ]\ \begin{itemize} \item Structured Communication-Centred Programming for Web Services \\ \sp 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 \\ \sp Maria Grazia Buscemi (IMT Lucca ) and Ugo Montanari (University of Pisa). \item A Calculus for Orchestration of Web Services \\ \sp Alessandro Lapadula (University of Florence), Rosario Pugliese (University of Florence) and Francesco Tiezzi (University of Florence). \item A Concurrent Calculus with Atomic Transactions \\ \sp Lucia Acciai (Laboratoire d'Informatique Fondamentale, Marseille), Silvano Dal Zilio (Laboratoire d'Informatique Fondamentale, Marseille) and Michele Boreale (University of Florence). \end{itemize} \item[FASE - Model Driven Development (Chair: Maura Cerioli) ]\ \begin{itemize} \item Integrating performance and reliability analysis in a Non-Functional MDA framework \\ \sp 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 \\ \sp 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 \\ \sp Rolf Hennicker (Ludwig-Maximilians-Universitat Munchen,Germany), Alexander Knapp (Ludwig-Maximilians-Universitat Munchen, Germany) \item Flexible and Extensible Notations for Modeling \\ \sp Jimin Gao (University of Minnesota, USA), Mats Heimdahl (University of Minnesota, USA), Eric Van Wyk (University of Minnesota, USA) \end{itemize} \item[FOSSACS - Automata (Chair: Markus Mueller-Olm) ]\ \begin{itemize} \item Tree Automata with Memory, Visibility and Structural Constraints \\ \sp Hubert Comon (ENS Cachan), Florent Jacquemard (INRIA/ENS Cachan), Nicolas Perrin (ENS Lyon) \item Model-Checking One-Clock Priced Timed Automata \\ \sp Patricia Bouyer (ENS Cachan), Nicolas Markey (ENS Cachan), Kim G. Larsen (Aalborg Univ.) \item Sampled Universality of Timed Automata \\ \sp Pavel Krcal (Uppsala Univ.), Wang Yi (Uppsala Univ.), Parosh Abdulla (Uppsala Univ.) \item A Lower Bound on Web Services Composition \\ \sp Anca Muscholl (LABRI, Bordeaux), Igor Walukiewiczi (LABRI, Bordeaux) \end{itemize} \item[FACAS - Abstraction Refinement (Chair: Shmuel Katz) ]\ \begin{itemize} \item Deciding Bit-Vector Arithmetic with Abstraction \\ \sp 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 \\ \sp Alessandro Armando (Universita di Genova), Massimo Benerecetti (Universita di Napoli), and Jacopo Mantovani (Universita di Genova) \item Property-Driven Partitioning for Abstraction Refinement \\ \sp 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 \\ \sp Nina Amla and Kenneth McMillan (Cadence Design Systems) \end{itemize} \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) ]\ \begin{itemize} \item Verifying object-oriented software: lessons and challenges \\ \sp K. Rustan M. Leino (Microsoft Research, Redmond, USA) \end{itemize} \end{description} \subsubsection*{15:40 - 15:50 Break } \subsubsection*{15:50 - 16:50 SESSION 3B (Wednesday)} \begin{description} \item[ESOP - Verification (Chair: Pierpaolo Degano) ]\ \begin{itemize} \item Modal I/O Automata for Interface and Product Line Theories \\ \sp Kim G. Larsen (Aalborg University), Ulrik Nyman (Aalborg University) and Andrzej Wasowski (IT University of Copenhagen) \item Using history invariants to verify observers \\ \sp Rustan Leino (Microsoft Research) and Wolfram Schulte (Microsoft Research) \end{itemize} \item[ESOP - Term Rewriting (Chair: Don Sannella) ]\ \begin{itemize} \item On the implementation of construction functions for non-free concrete data types \\ \sp Frederic Blanqui (INRIA), Therese Hardin (Universite Paris 6) and Pierre Weis (INRIA) \item Anti-Pattern Matching \\ \sp Claude Kirchner (INRIA-LORIA Nancy), Radu Kopetz (INRIA-LORIA Nancy) and Pierre-Etienne Moreau (INRIA-LORIA Nancy) \end{itemize} \item[FASE - Tool Demonstrations (Chair: Jos\'e Nuno Oliveira) ]\ \begin{itemize} \item Declared Type Generalization Checker: An Eclipse Plug-In for Programming with More General Types \\ \sp Markus Bach (University of Hagen, Germany), Florian Forster (University of Hagen, Germany), Friedrich Steimann (University of Hagen, Germany) \item S2A: A Compiler for Multi-Modal UML Sequence Diagrams \\ \sp David Harel (The Weizmann Institute of Science, Israel), Asaf Kleinbort (The Weizmann Institute of Science, Israel), Shahar Maoz (The Weizmann Institute of Science, Israel) \end{itemize} \item[TACAS - Message Sequence Charts (Chair: Nina Amla) ]\ \begin{itemize} \item Detecting Races in Ensembles of Message Sequence Charts \\ \sp 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 \\ \sp Benedikt Bollig (LSV CNRS Cachan), Joost-Pieter Katoen, Carsten Kern (RWTH Aachen University), and Martin Leucker (TU Munich) \end{itemize} \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) ]\ \begin{itemize} \item A Certified Lightweight Non-Interference Java Bytecode Verifier \\ \sp 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 \\ \sp Heiko Mantel (RWTH Aachen University) and Alexander Reinhard (RWTH Aachen University) \item Cost Analysis of Java Bytecode \\ \sp 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) \end{itemize} \item[ESOP - Logics and Correctness Proofs (Chair: Walid Taha) ]\ \begin{itemize} \item On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning \\ \sp Xinyu Feng (Yale University), Rodrigo Ferreira (Yale University) and Zhong Shao (Yale University) \item Abstract Predicates and Mutable ADTs in Hoare Type Theory \\ \sp 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 \\ \sp Guodong Li (University of Utah) and Konrad Slind (University of Utah) \end{itemize} \item[FASE - Distributed Systems (Chair: Holger Giese) ]\ \begin{itemize} \item Scenario-Driven Dynamic Analysis of Distributed Architectures \\ \sp 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 \\ \sp 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 \\ \sp C\'esar Sanchez (Stanford University, USA), Henny B. Sipma (Stanford University, USA), Zohar Manna (Stanford University, USA) \end{itemize} \item[TACAS - Automata-Based Model Checking (Chair: Daniel Kroening) ]\ \begin{itemize} \item Improved algorithms for the automata based approach to model-checking \\ \sp Laurent Doyen (EPFL) and Jean-Francois Raskin (Universitat Libre de Bruxelles) \item GOAL: A Graphical Tool for Manipulating Buechi Automata and Temporal Formulae \\ \sp 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 \\ \sp Florian Horn (LIAFA, Universite Paris 7) \end{itemize} \end{description} \subsubsection*{19:00 SOCIAL EVENT (Wednesday)} \begin{description} \item[Conference Banquet (tickets needed) ]\item \emph{Pa\c{c}o dos Duques} , Guimar\~aes \item Shuttle departure from \emph{Theatro Circo} \end{description} \newpage \subsubsection{Thursday, March 29} \subsubsection*{09:00 - 10:00 SESSION 1 (Thursday)} \begin{description} \item[FASE - Invited Talk (Chair: Matt Dwyer) ]\ \begin{itemize} \item Software Product Families: Towards Compositionality \\ \sp Jan Bosch (Nokia, Finland) \end{itemize} \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) ]\ \begin{itemize} \item Modular Shape Analysis for Dynamically Encapsulated Programs \\ \sp 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 \\ \sp Stephane Gaubert (INRIA), Eric Goubault (CEA/Saclay), Ankur Taly (IIT Bombay) and Sarah Zennou (CEA/Saclay) \item Computing Procedure Summaries for Interprocedural Analysis \\ \sp Sumit Gulwani (Microsoft Research) and Ashish Tiwari (SRI International) \item Small witnesses for abstract interpreation based proofs \\ \sp Fr\'ed\'eric Besson (Irisa/Inria), Thomas Jensen (Irisa/CNRS) and Tiphaine Turpin (Irisa/Universit\'e de Rennes 1) \end{itemize} \item[FASE - Specification (Chair: Marsha Chechik) ]\ \begin{itemize} \item Precise Specification of Use Case Scenarios \\ \sp Jon Whittle (George Mason University, USA) \item Joint Structural and Temporal Property Specification using Timed Story Sequence Diagrams \\ \sp Florian Klein (University of Paderborn, Germany), Holger Giese (University of Paderborn, Germany) \item SDL Profiles - Formal Semantics and Tool Support \\ \sp 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 \\ \sp Lilian Burdy (INRIA Sophia Antipolis, France), Marieke Huisman (INRIA Sophia Antipolis, France), Mariele Pavlova (INRIA Sophia Antipolis, France) \end{itemize} \item[TACAS - Specification Languages (Chair: Marsha Chechik) ]\ \begin{itemize} \item Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based Programs \\ \sp David Harel and Itai Segall (The Weizmann Institute of Science) \item MoToR: The MoDeST Tool Environment \\ \sp 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 \\ \sp Alessandro Cimatti, Marco Roveri (ITC-irst Trento), and Stefano Tonetta (University of Lugano) \item The Heterogeneous Tool Set \\ \sp Till Mossakowski, Christian Maeder (DFKI Lab and University of Bremen), and Klaus Luettich (SFB/TR 8 and University of Bremen) \end{itemize} \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) ]\ \begin{itemize} \item Contract-Driven Development \\ \sp Bertrand Meyer (ETH Z\"urich, Switzerland) \end{itemize} \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) ]\ \begin{itemize} \item Interprocedurally analyzing linear inequality relations \\ \sp Hemut Seidl (Lehrstuhl Seidl, TUM) , Andrea Flexeder (TU Munich) and Michael Petter. (TU Munich) \item Precise Fixpoint Computation Through Strategy Iteration \\ \sp Thomas Gawlitza (Lehrstuhl Seidl, TUM) and Hemut Seidl (Lehrstuhl Seidl, TUM) \end{itemize} \item[TACAS - Security (Chair: Michael Huth) ]\ \begin{itemize} \item Searching for Shapes in Cryptographic Protocols \\ \sp 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 \\ \sp Veronique Cortier (Loria and CNRS and INRIA), Gavin Keighren, and Graham Steel (University of Edinburgh) \end{itemize} \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) ]\ \begin{itemize} \item A Complete Guide to the Future \\ \sp Frank S. de Boer (CWI), Dave Clarke (CWI) and Einar Broch Johnsen (University of Oslo) \item The Java Memory Model: Operationally, Denotationally, Axiomatically \\ \sp 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 \\ \sp Christian Haack (Radboud Universiteit, Nijmegen), Erik Poll (Radboud Universiteit, Nijmegen), Jan Schaefer (TU Kaiserslautern) and Aleksy Schubert (Radboud Universiteit, Nijmegen) \end{itemize} \item[FASE - Services (Chair: Jos\'e Fiadeiro) ]\ \begin{itemize} \item A Service Composition Construct to Support Iterative Development \\ \sp Roy Gronmo (SINTEF, Norway), Michael C. Jaeger (Technical University Berlin, Germany), Andreas Wombacher (University Twente, The Netherlands) \item Correlation Patterns in Service-Oriented Architectures \\ \sp 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 \\ \sp Marc Fisher II (University of Nebraska-Lincoln, USA), Sebastian Elbaum (University of Nebraska-Lincoln, USA), Gregg Rothermel (University of Nebraska-Lincoln, USA) \end{itemize} \item[TACAS - Software and Hardware Verification (Chair: Orna Grumberg) ]\ \begin{itemize} \item State of the Union: Type Inference via Craig Interpolation \\ \sp Ranjit Jhala (UC San Diego), Rupak Majumdar, and Ru-Gang Xu (UC Los Angeles) \item Hoare Logic for Realistically Modelled Machine Code \\ \sp Magnus O. Myreen and Michael J. C. Gordon (University of Cambridge) \item VCEGAR: Verilog CounterExample Guided Abstraction Refinement \\ \sp 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{itemize} \end{description} \newpage \subsubsection{Friday, March 30} \subsubsection*{09:00 - 10:00 SESSION 1 (Friday)} \begin{description} \item[ESOP - Invited Talk (Chair: Rocco De Nicola) ]\ \begin{itemize} \item Techniques for Contextual Equivalence in Higher-Order, Typed Languages \\ \sp Andrew Pitts (University of Cambridge, UK) \end{itemize} \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) ]\ \begin{itemize} \item Scalar Outcomes Suffice for Finitary Probabilistic Testing \\ \sp 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 \\ \sp Ichiro Hasuo (Radboud University Nijmegen) and Yoshinobu Kawabe (NTT Corporation) \item Proving Distributed Algorithm Correctness using Fault Tolerance Bisimulations \\ \sp Adrian Francalanza (Imperial College) and Matthew Hennessy (University of Sussex) \item A core calculus for a comparative analysis of bio-inspired calculi \\ \sp Cristian Versari (University of Bologna) \end{itemize} \item[FASE - Testing (Chair: Reiko Heckel) ]\ \begin{itemize} \item A Prioritization Approach for Software Test Cases Based on Bayesian Networks \\ \sp Siavash Mirarab (University of Waterloo, Canada), Ladan Tahvildari (University of Waterloo, Canada) \item Redundancy Based Test-Suite Reduction \\ \sp Gordon Fraser (Graz University of Technology, Austria), Franz Wotawa (Graz University of Technology, Austria) \item Testing Scenario-Based Models \\ \sp 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 \\ \sp 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) \end{itemize} \item[TACAS - Decision Procedures and Theorem Provers (Chair: Parosh Abdulla) ]\ \begin{itemize} \item Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications \\ \sp Marcelo F. Frias, Carlos G. Lopez Pombo, and Mariano M. Moscato (Universidad de Buenos Aires and CONICET) \item Combined Satisfiability Modulo Parametric Theories \\ \sp Sava Krstic, Amit Goel, Jim Grundy (Intel Corporation), and Cesare Tinelli (The University of Iowa) \item A Groebner Basis Approach to CNF-formulae Preprocessing \\ \sp Christopher Condrat and Priyank Kalla (University of Utah) \item Kodkod: A Relational Model Finder \\ \sp Emina Torlak and Daniel Jackson (Massachusetts Institute of Technology) \end{itemize} \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) ]\ \begin{itemize} \item A Rewriting Semantics for Type Inference \\ \sp George Kuan (University of Chicago), David MacQueen (University of Chicago) and Robert Bruce Findler (University of Chicago) \item Principal Type Schemes for Modular Programs \\ \sp Derek Dreyer (Toyota Technological Institute at Chicago) and Matthias Blume (Toyota Technological Institute at Chicago) \item A Consistent Semantics of Self-Adjusting Computation \\ \sp Umut Acar (Toyota Technological Institute at Chicago), Matthias Blume (Toyota Technological Institute at Chicago) and Jacob Donham (Carnegie Mellon University) \item Multi-Language Synchronization \\ \sp Robert Ennals (Intel Research, Berkeley) and David Gay (Intel Research, Berkeley) \end{itemize} \item[FASE - Analysis (Chair: Tom Maibaum) ]\ \begin{itemize} \item Practical reasoning about invocations and implementations of pure methods \\ \sp \'Ad\'am Darvas (ETH Zurich, Switzerland), K. Rustan M. Leino (Microsoft Research, USA) \item Finding Environment Guarantees \\ \sp 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 \\ \sp Ulrike Ranger (RWTH Aachen University, Germany), Thorsten Hermes (RWTH Aachen University, Germany) \item Maintaining Consistency in Layered Architectures of Mobile Ad-hoc Networks \\ \sp 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) \end{itemize} \item[TACAS - Model Checking (Chair: Orna Grumberg) ]\ \begin{itemize} \item Bounded Reachability Checking of Asynchronous Systems Using Decision Diagrams \\ \sp Jinqing Yu, Gianfranco Ciardo (University of California, Riverside), and Gerald Luettgen (University of York) \item Model Checking of Tree Logics with Path Equivalences \\ \sp Rajeev Alur, Pavol Cerny, and Swarat Chaudhuri (University of Pennsylvania) \item Uppaal/DMC - Abstraction-based Heuristics for Directed Model Checking \\ \sp 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 \\ \sp 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{itemize} \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) ]\ \begin{itemize} \item Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts \\ \sp Kohei Suenaga (University of Tokyo) and Naoki Kobayashi (Tohoku University) \item Type Reconstruction for an Undecidable System of Refinement Types \\ \sp Kenneth Knowles (University of California, Santa Cruz) and Cormac Flanagan (University of California, Santa Cruz) \item Dependent Types for Low-Level Programming \\ \sp 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) \end{itemize} \item[FASE - Design (Chair: Ant\'onia Lopes) ]\ \begin{itemize} \item Towards Normal Design for Safety-Critical Systems \\ \sp 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 \\ \sp 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 \\ \sp Roberto E. Lopez-Herrejon (University of Oxford, England), Sven Apel (University of Magdeburg, Germany) \end{itemize} \item[TACAS - Infinite-State Systems (Chair: Michael Huth) ]\ \begin{itemize} \item A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes \\ \sp Ahmed Bouajjani, Yan Jurski, and Mihaela Sighireanu (LIAFA, University of Paris 7) \item Unfolding Concurrent Well-Structured Transition Systems \\ \sp Frederic Herbreteau, Gregoire Sutre, and The Quang Tran (LaBRI, Bordeaux) \item Regular Model Checking without Transducers (On Efficient Verification of Parameterized Systems) \\ \sp Parosh Aziz Abdulla (Uppsala University), Giorgio Delzanno (Universita di Genova), Noomene Ben Henda, and Ahmed Rezine (Uppsala University) \end{itemize} \end{description} \newpage \section{Workshops} %\subsection{Short description} \begin{itemize} \item \textbf{ACCAT} , Applied and Computational Category Theory \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\texttt{++}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} \textbf{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*{ByteCode} \textbf{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} \textbf{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} \textbf{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} \textbf{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} \textbf{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} \textbf{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} \textbf{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} \textbf{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} \textbf{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/} \newpage \mbox{}\hspace{1.5cm}\includegraphics[width=16.2cm,height=22cm]{left-etaps} {\bf Where: \verb! ! S1 -- Enabler Wipro Room (Grand Auditorium) \verb! ! S2 -- Cisco Room (Main Hall) \verb! ! S3 -- Multicert Room (Second Auditorium) \verb! ! S4 -- Unicre Room (Rehearsal Room) } \newpage \mbox{}\hspace{-1.5cm}\includegraphics[width=18.3cm,height=22cm]{right-etaps} \newpage \subsubsection*{MOMPES} \textbf{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} \textbf{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} \textbf{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} \textbf{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\texttt{++}P} \textbf{Model-driven High-level Programming of Embedded Systems} SLA\texttt{++}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\texttt{++}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} \textbf{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} \textbf{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 \newpage \subsection{Programme of ACCAT} \subsubsection*{Applied and Computational Category Theory} \subsubsection*{Sunday, March 25, room: CP2-103} \subsubsection*{09:00 - 10:15 SESSION 1} \begin{itemize} \item Introduction \item Generalized Sketches - A Universal Pattern for Diagrammatic Specification \\ \sp Uwe Wolter \item Dynamics and Cohesion in Finite Toposes \\ \sp William Lawvere \end{itemize} \subsubsection*{10:15 - 11:00 Coffee Break} \subsubsection*{11:00 - 12:30 SESSION 2} \begin{itemize} \item Normalized Coalgebras for Dynamic Bisimilarity \\ \sp Ugo Montanari \item Structured Co-spans: Algebraic Modelling of Interaction Protocols \\ \sp Jos\'e Fiadeiro \item Iterative Algebras \\ \sp Jiri Adamek \end{itemize} \subsubsection*{12:30 - 14:00 Lunch} \subsubsection*{15:00 - 16:00 SESSION 3} \begin{itemize} \item A Categorical Model of Computation for Graph Transformation: True Concurrency and Logic \\ \sp Reiko Heckel \item Adhesive High-Level Replacement Systems with Negative Application Conditions \\ \sp Leen Lambers \item Composing DPO Transformations with Borrowed Context \\ \sp Paolo Baldan \item Algebraic High-Level Systems as Weak Adhesive HLR Categories \\ \sp Ulrike Prange \end{itemize} \subsubsection*{16:00 - 16:30 Coffee Break} \subsubsection*{16:30 - 18:00 SESSION 4} \begin{itemize} \item Categories in the Design of Aldor \\ \sp Stephen Watt \item (tba) \\ \sp Vladimiro Sassone \item (tba) \\ \sp Jochen Pfalzgraf \end{itemize} \newpage \subsection{Programme of Bytecode } \subsubsection*{Second Workshop on Bytecode Semantics, Verification, Analysis and Transformation} \subsubsection*{Saturday, March 31, room: CP2-103} \subsubsection*{09:00 - 10:30 SESSION 1} \textbf{Session Chair: Marieke Huisman} \begin{itemize} \item Invited Talk: Modular verification of object invariants in Spec\# \\ \sp Peter M\"uller (ETH Zurich) \item Type Systems for optimising Stack-based Code \\ \sp Tarmo Uustalu and Ando Saabas (Tallinn University of Technology, Estonia) \end{itemize} \subsubsection*{10:30 - 11:00 Coffee Break} \subsubsection*{11:00 - 12:30 SESSION 2} \begin{itemize} \item Proving Resource Consumption of Low-level and Programs using Automated Theorem Provers \\ \sp Jaroslav Sevcik (University of Edinburgh, UK) \item Formal Translation of Bytecode into BoogiePL \\ \sp Hermann Lehner and Peter M\"uller (ETH, Zurich, Switzerland) \item Bytecode Rewriting in Tom \\ \sp Emilie Balland, Pierre-Etienne Moreau and Antoine Reilles (Loria, France) \end{itemize} \subsubsection*{12:30 - 14:00 Lunch} \subsubsection*{14:00 - 16:00 SESSION 3} \textbf{Session Chair: Peter M\"uller} \begin{itemize} \item Translate One, Analyze Many: Leveraging the Microsoft Intermediate Language and Source Code Transformation for Model Checking \\ \sp Jesse McGeachie and Juergen Dingel (Queen's University, Canada) \item Practical Assessment of Cost Analysis for Java Bytecode \\ \sp 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 \\ \sp 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 \\ \sp Miguel Gomez-Zamalloa, Elvira Albert and German Puebla (Universidad Polit\'ecnica de Madrid, Universidad Complutense de Madrid, Spain) \end{itemize} \subsubsection*{16:00 - 16:30 Coffee Break} \subsubsection*{16:30 - 17:30 SESSION 4} \textbf{Session Chair: Fausto Spoto} \begin{itemize} \item Computing SSA Form with Matrices \\ \sp 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 \\ \sp Mario M\'endez, Jorge Navas and Manuel Hermenegildo (University of New Mexico, USA) \end{itemize} \newpage \subsection{Programme of COCV } \subsubsection*{Compiler Optimization meets Compiler Verification} \subsubsection*{Sunday, March 25, room: CP2-108} \subsubsection*{09:00 - 10:30 SESSION 1} \textbf{Opening} \begin{itemize} \item Jens Knoop, Vienna University of Technology \end{itemize} \textbf{Invited Talk} \begin{itemize} \item High-Level vs. RTL Equivalence Checking: Why the Next Big Success of Formal Verification Needs COCV \\ \sp Alan Hu, University of British Columbia, Canada \end{itemize} \subsubsection*{10:30 - 11:00 Coffee Break} \subsubsection*{11:00 - 12:00 SESSION 2} \begin{itemize} \item Specify, Compile, Run: Hardware from PSL \\ \sp Bloem, Galler, Jobstmann, Piterman, Pnueli, Weiglhofer (Graz University of Technology, Austria; EPFL Lausanne, Switzerland; Weizmann Institute, Israel) \end{itemize} \subsubsection*{12:30 - 14:00 Lunch} \subsubsection*{14:00 - 16:00 SESSION 3} \begin{itemize} \item Distilling Programs for Verification \\ \sp Geoff Hamilton (Dublin City University, Ireland) \item On-the-Fly Data Flow Analysis based on Verification Technology \\ \sp Mar\`ia del Mar Gallardo, Christophe Joubert and Pedro Merino (University of M\'alaga, Spain) \end{itemize} \subsubsection*{16:00 - 16:30 Coffee Break} \subsubsection*{16:30 - 18:00 SESSION 4} \begin{itemize} \item Generating Java Compiler Optimizers Using Bidirectional CTL \\ \sp Ling Fang and Masataka Sassa (Tokyo Institute of Technology, Japan) \item A Certifying Code Generation Phase \\ \sp Jan Olaf Blech and Arnd Poetzsch-Heffter (University of Kaiserslautern, Germany) \end{itemize} \subsubsection*{16:30 - 18:00 Closure} \newpage \subsection{Programme of FESCA } \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 ]\ \begin{itemize} \item SENSORIA: Semantic-based Development of Service-Oriented Systems \\ \sp Martin Wirsing (LMU) \end{itemize} \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 ]\ \begin{itemize} \item A True-Concurrent Interpretation of Behavioural Scenarios \\ \sp Sotiris Moschoyiannis, Paul Krause and Michael Shields \item Trustworthy interface compliancy: data model adaptation using B refinement \\ \sp Samuel Colin, Arnaud Lanoix, Jeanine Souquieres \item Towards Component Verification in the Generic Component Framework \\ \sp Julia Padberg, Hartmut Ehrig, Fernando Orejas \end{itemize} \end{description} \subsubsection*{12:30 - 14:00 Lunch} \subsubsection*{14:00 - 16:00 SESSION 3} \begin{description} \item[Behavioural models ]\ \begin{itemize} \item DeSpec: Modeling the Windows Driver Environment \\ \sp Tomas Matousek and Pavel Jezek \item WCET Analysis of Data Dependent, Component Oriented, Embedded Software Systems \\ \sp Peter Szulman \item Composing Modal Properties of Programs with Procedures \\ \sp Marieke Huisman, Dilian Gurov \end{itemize} \end{description} \subsubsection*{16:00 - 16:30 Coffee Break} \subsubsection*{16:30 - 17:30 SESSION 4} \begin{description} \item[Contractual runtime verification ]\ \begin{itemize} \item A Formal Semantics for a Quality of Service Contract Language \\ \sp Fabricio Chalub, Alexandre Sztajnberg \item Executable Contracts for Incremental Prototypes of Embedded Systems \\ \sp Lionel Morel and Louis Mandel \end{itemize} \end{description} \subsubsection*{17:30 Concluding Remarks} \newpage \subsection{Programme of FinCo } \subsubsection*{Foundations of Interactive Computation} \subsubsection*{Saturday, March 31, room: CP2-106} \subsubsection*{09:00 - 10:30 SESSION 1} \begin{description} \item[Welcome ]\item[Invited Talk ]\ \begin{itemize} \item Event-driven Design in Practice and Theory \\ \sp Bertrand Meyer, ETH Zurich and Eiffel Software \end{itemize} \end{description} \subsubsection*{10:30 - 11:00 Coffee Break} \subsubsection*{11:00 - 12:30 SESSION 2} \begin{description} \item[Specification and Analysis of Interactive Agents ]\ \begin{itemize} \item A Formal Framework for Interactive Agents \\ \sp Carolyn L. Talcott (SRI International, USA) \item Observable Behavior of Dynamic Systems: Component-Based Reasoning for Concurrent Objects \\ \sp Johan Dovland, Einar Broch Johnsen, and Olaf Owe (Univ. Oslo, Norway) \end{itemize} \end{description} \subsubsection*{12:30 - 14:00 Lunch} \subsubsection*{14:00 - 16:00 SESSION 3} \begin{description} \item[Modeling Interaction ]\ \begin{itemize} \item Interaction in Time and Space \\ \sp Gabriel Ciobanu (A.I.Cusa Univ., Romania) \item Validating for Liveness in Hidden Adversary Systems \\ \sp Saikat Mukherjee, Srinath Srinivasa, and SatishChandra D. (IIIT Bangalore, India) \item AGAPIA v0.1: A Programming Language for Interactive Systems and its Typing System \\ \sp Cezara Dragoi and Gheorghe Stefanescu (Univ. Bucharest, Romania) \end{itemize} \end{description} \subsubsection*{16:00 - 16:30 Coffee Break} \subsubsection*{16:30 - 18:30 SESSION 4} \begin{description} \item[Programming Languages for Interactive Computing ]\ \begin{itemize} \item Programming Languages for Interactive Computing \\ \sp Roly Perera \end{itemize} \item[Panel Discussion ]\ \begin{itemize} \item Models and Languages for Interactive Systems \\ \sp all speakers \end{itemize} \item[Closing ]\ \begin{itemize} \item Dina Goldin (Brown University, USA) \end{itemize} \end{description} \newpage \subsection{Programme of GT-VMT } \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 ]\ \begin{itemize} \item Membrane Computing [and Graph Transformation] \\ \sp Gheorghe Paun (Romanian Academy and Sevilla University, Spain) \end{itemize} \end{description} \subsubsection*{10:30 - 11:00 Coffee Break} \subsubsection*{11:00 - 12:30 SESSION 2} \begin{description} \item[Verification and Model Transformation ]\ \begin{itemize} \item Rule-Level Verification of Business Process Transformations using CSP \\ \sp D\'enes Bisztray, Reiko Heckel \item Bisimulation Verification for the DPO Approach with Borrowed Contexts \\ \sp Guilherme Rangel, Barbara K\"onig, Hartmut Ehrig \item Transforming Collaborative Service Specifications into Efficiently Executable State Machines \\ \sp Frank Alexander Kraemer, Peter Herrmann \end{itemize} \end{description} \subsubsection*{12:30 - 14:15 Lunch} \subsubsection*{14:15 - 16:00 SESSION 3} \begin{description} \item[Pattern Matching ]\ \begin{itemize} \item Ensuring Containment Constraints in Graph-based Model Transformation Approaches (Short Talk) \\ \sp Christian K\"ohler, Holger Lewin, Gabriele Taentzer \item Generic Search Plans for Matching Advanced Graph Patterns \\ \sp \'Akos Horv\'ath, Gergely Varr\'o, D\'aniel Varr\'o \item A Query Language With the Star Operator \\ \sp Johan Lindqvist, Torbj\"orn Lundkvist, Ivan Porres \item Triple Patterns: Compact Specifications for the Generation of Operational Triple Graph Grammar Rules \\ \sp Juan de Lara, Esther Guerra, Paolo Bottoni \end{itemize} \end{description} \subsubsection*{16:00 - 16:30 Coffee Break} \subsubsection*{16:30 - 18:00 SESSION 4} \begin{description} \item[Graph Transformation Language Operations ]\ \begin{itemize} \item A Subgraph Operator for Graph Transformation Languages \\ \sp Daniel Balasubramanian, Anantha Narayanan, Sandeep Neema, Feng Shi, Ryan Thibodeaux, Gabor Karsai \item Adding Recursion to Graph Transformation \\ \sp Esther Guerra, Juan de Lara \item Visual Programming with Recursion Patterns in Interaction Nets \\ \sp Ian Mackie, Jorge Sousa Pinto, Miguel Vila\c{c}a \item Simulating Multi-graph Transformations Using Simple Graphs (Short Talk) \\ \sp Frank Hermann, Harmen Kastenberg, Iovka Boneva, Arend Rensink \end{itemize} \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 ]\ \begin{itemize} \item Evaluating Workflow Definition Language Revisions with Graph-Based Tools \\ \sp 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) \\ \sp Gregor Wrobel, Ralf-Erik Ebert, Matthias Ple"sow \item Imposing Hierarchy on a Graph (Short Talk) \\ \sp Brendan Sheehan, Benoit Gaudin, Aaron Quigley \item The Jury is still out: A Comparison of AGG, Fujaba, and PROGRES (Short Talk) \\ \sp Ulrike Ranger, Christian Fu"s, Christof Mosler, Erhard Schultchen \end{itemize} \end{description} \subsubsection*{12:30 - 14:15 Lunch} \subsubsection*{14:15 - 16:00 SESSION 3} \begin{description} \item[Working Groups ]\ \begin{itemize} \item Building of Working Groups \item Discussion in Working Groups \item General Discussion of the Results \end{itemize} \item[Closing ] \end{description} \newpage \subsection{Programme of HAV} \subsubsection*{Heap Analysis and Verification} \subsubsection*{Sunday, March 25, room: CP2-104} \subsubsection*{09:00 - 10:30 SESSION 1} \begin{itemize} \item Footprint Analysis: A Shape Analysis that Discovers Preconditions (Invited Lecture) \\ \sp Hongseok Yang \item Proof Systems for Inductive Reasoning in the Logic of Bunched Implications \\ \sp James Brotherston \end{itemize} \subsubsection*{10:30 - 11:00 Coffee Break} \subsubsection*{11:00 - 12:30 SESSION 2} \begin{itemize} \item A Logic of Reachable Patterns (Invited Lecture) \\ \sp Greta Yorsh \item Verifying Complex Properties using Symbolic Shape Analysis \\ \sp Thomas Wies, Viktor Kuncak, Karen Zee, Martin Rinard and Andreas Podelski \end{itemize} \subsubsection*{12:30 - 14:00 Lunch} \subsubsection*{14:00 - 16:00 SESSION 3} \begin{itemize} \item Alias Control with Universe Types (Invited Lecture) \\ \sp Peter M\"uller \item Inferring Local (Non-)Aliasing and Strings for Memory Safety \\ \sp Yannick Moy and Claude March\'e \item Reasoning about Sequences of Memory States \\ \sp Brochenin R\'emi, Demri St\'ephane and Lozes \'Etienne \end{itemize} \subsubsection*{16:00 - 16:30 Coffee Break} \subsubsection*{16:30 - 18:00 SESSION 4} \begin{itemize} \item Liveness of Heap Data for Functional Programs \\ \sp Amey Karkare, Uday Khedker and Amitabha Sanyal \item Separation Analysis for Deductive Verification \\ \sp Thierry Hubert and Claude March\'e \item Verifying Concurrent List-Manipulating Programs by LTL Model Checking \\ \sp Stefan Rieger, Thomas Noll and Joost-Pieter Katoen \item Towards Regional Logic (Invited Lecture) \\ \sp David Naumann \end{itemize} \newpage \subsection{Programme of HFL } \subsubsection*{Hardware design using Functional Languages} \subsubsection*{Saturday, March 24, room: CP2-110} \subsubsection*{09:00 - 10:30 SESSION 1} \begin{itemize} \item Introducing Scheduling Primitives and Derived Interfaces in Bluespec \\ \sp Arvind, Nirav Dave, and Michael Pellauer (MIT) \item Declarative Programming Techniques for Many-Core Architectures \\ \sp Satnam Singh (Microsoft Research Cambridge) \end{itemize} \subsubsection*{10:30 - 11:00 Coffee Break} \subsubsection*{11:00 - 12:30 SESSION 2} \begin{itemize} \item Searching for prefix networks to fit in a context using a lazy functional programming language \\ \sp Mary Sheeran (Chalmers) \item The E Language \\ \sp Robert S. Boyer and Warren A. Hunt, Jr. (University of Texas) \end{itemize} \subsubsection*{12:30 - 14:30 Lunch and time for discussion} \subsubsection*{14:30 - 16:00 SESSION 3} \begin{itemize} \item A framework for designing hardware in Ocaml \\ \sp Andrew K. Martin and Ahmed Gheith (IBM) \item High-Level Micro-Architectural Transformations and Cycle-Accurate High-Level Models \\ \sp Carl-Johan H. Seger (Intel) \end{itemize} \subsubsection*{16:00 - 16:30 Coffee Break} \subsubsection*{16:30 - 18:00 SESSION 4} \begin{itemize} \item Functional Programming for Hardware Definition, Verification and Modelling \\ \sp Nathan Chong and Samin Ishtiaq (ARM) \item Program Transformation for Functional Circuit Descriptions \\ \sp Manfred Schmidt-Schau"s and David Sabel (Johann Wolfgang Goethe-Universit"st) \end{itemize} \subsubsection*{Sunday, March 25, room: CP2-110} \subsubsection*{09:00 - 10:30 SESSION 1} \begin{itemize} \item Embedded Hardware Description Languages: Exploring the Design Space \\ \sp Koen Claessen (Chalmers) and Gordon Pace (University of Malta) \item Lightweight Relational Programming for Wired \\ \sp Matthew Naylor (University of York), Emil Axelsson (Chalmers), and Colin Runciman (University of York) \end{itemize} \subsubsection*{10:30 - 11:45 Coffee Break and Demos} \subsubsection*{11:45 - 12:30 SESSION 2} \begin{itemize} \item Towards Automatically Compiling Efficient FPGA Hardware \\ \sp Jean Baptiste Note and Jean Vuillemin (Ecole Normale Sup\'erieure Paris) \end{itemize} \subsubsection*{12:30 - 14:30 Lunch and time for discussion} \subsubsection*{14:30 - 16:00 SESSION 3} \begin{itemize} \item Design Principles for Hardware Description \\ \sp Tim Sheard (Portland State University) \item Hardware descriptions as two-level computations \\ \sp 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{itemize} \subsubsection*{15:15 - 16:30 Coffee, demos, planning of next workshop} \newpage \subsection{Programme of LDTA } \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 ]\ \begin{itemize} \item Collaboration-Based Composition of Languages \\ \sp Uwe A"smann \end{itemize} \item[Research Talk ]\ \begin{itemize} \item Language Parametric Module Management \\ \sp Paul Klint, Taeke Kooiker, Jurgen Vinju \end{itemize} \end{description} \subsubsection*{10:30 - 11:00 Coffee Break} \subsubsection*{11:00 - 12:30 SESSION 2} \begin{description} \item[Research Talk ]\ \begin{itemize} \item Fusing a Transformation Language with an Open Compiler \\ \sp Karl Trygve Kalleberg, Eelco Visser \end{itemize} \item[Experience Report ]\ \begin{itemize} \item Implementing a Domain-Specific Language using Stratego/XT \\ \sp Leonard Hamey, Shirley Goldrei \end{itemize} \item[Tool Demonstration ]\ \begin{itemize} \item Spoofax: An Interactive Development Environment for Program Transformation with Stratego/XT \\ \sp Karl Trygve Kalleberg, Eelco Visser \end{itemize} \end{description} \subsubsection*{12:30 - 14:00 Lunch} \subsubsection*{14:00 - 16:00 SESSION 3} \begin{description} \item[Research Talk ]\ \begin{itemize} \item SPPF-Style Parsing From Earley Recognisers \\ \sp Elizabeth Scott \end{itemize} \item[Experience Report ]\ \begin{itemize} \item An Experimental Ambiguity Detection Tool \\ \sp Sylvain Schmitz \end{itemize} \item[Research Talk ]\ \begin{itemize} \item Grammar Engineering Support for Precedence Rule Recovery and Compatibility Checking \\ \sp Eric Bouwers, Martin Bravenboer, Eelco Visser \end{itemize} \item[Tool Demonstration ]\ \begin{itemize} \item SdfMetz: Extraction of Metrics and Graphs From Syntax Definitions \\ \sp Tiago Alves, Joost Visser \end{itemize} \end{description} \subsubsection*{16:00 - 16:30 Coffee Break} \subsubsection*{16:30 - 18:15 SESSION 4} \begin{description} \item[Research Talk ]\ \begin{itemize} \item Silver: an Extensible Attribute Grammar System \\ \sp Eric Van Wyk, Derek Bodin, Jimin Gao, Lijesh Krishnan \end{itemize} \item[Experience Report ]\ \begin{itemize} \item Development of a Modelica Compiler using JastAdd \\ \sp Johan {\AA}kesson, Torbj\"orn Ekman, G\"orel Hedin \end{itemize} \item[Tool Demonstration ]\ \begin{itemize} \item A Domain-Specific Language Debugging Framework Demonstration \\ \sp Hui Wu, Jeff Gray, Marjan Mernik \end{itemize} \item[Discussion and Closing ] \end{description} \newpage \subsection{Programme of MBT } \subsubsection*{3rd Workshop on Model Based Testing} \subsubsection*{March 31, April 1, room: CP2-102\\09:00 - 10:30 SESSION 1} \textbf{Opening and Welcome} \begin{itemize} \item Bernd Finkbeiner, Yuri Gurevich, Alexander K. Petrenko \end{itemize} \textbf{Invited Talk} \begin{itemize} \item Finding a Good Order for Applying Adaptive Test Cases Rob Hierons \end{itemize} \subsubsection*{10:30 - 11:00 Coffee Break\\11:00 - 12:30 SESSION 2} \begin{itemize} \item A Global Algorithm for Model-Based Test Suite Generation Anders Hessel and Paul Pettersson \item Can a Model Checker Generate Tests for Non-Deterministic Systems? Sergiy Boroday, Alexandre Petrenko, and Roland Groz \end{itemize} \subsubsection*{12:30 - 14:30 Lunch\\14:30 - 16:00 SESSION 3} \begin{itemize} \item Generating Scenarios by Multi-Object Checking Maik Kollmann and Yuen Man Hon \item Testing Planning Domains (without Model Checkers) Franco Raimondi, Charles Pecheur, and Guillaume Brat \end{itemize} \subsubsection*{16:00 - 16:30 Coffee Break\\16:30 - 17:15 SESSION 4} \begin{itemize} \item Towards the Integration of Visual and Formal Models for GUI Testing Ana C. R. Paiva, João C. P. Faria, and Raul F. A. M. Vidal \end{itemize} \subsubsection*{17:15 - 18:00 Reserved} \subsection*{Sunday, April 1, room: CP2-102} \subsubsection*{09:00 - 10:30 SESSION 1} \textbf{Invited Talk} \begin{itemize} \item Model-Based Testing in the Standardization of Information and Communication Technologies: the ETSI Perspective Antti Huima \end{itemize} \subsubsection*{10:30 - 11:00 Coffee Breaks\\11:00 - 12:30 SESSION 2} \begin{itemize} \item Measuring a Java Test Suite Coverage using JML Specifications Frédéric Dadeau, Yves Ledru, and Lydie du Bousquet \item A Case Study in Matching Test and Proof Coverage Lydie du Bousquet, Yves Ledru, Frédéric Dadeau, and Faryel Allouti \end{itemize} \subsubsection*{12:30 - 14:30 Lunch\\14:30 - 16:00 SESSION 3} \begin{itemize} \item Automated Verification of Completeness and Consistency of Abstract State Machine Specifications using a SAT Solver Martin Ouimet and Kristina Lundqvist \item Handling Model Changes: Regression Testing and Test-Suite Update with Model-Checkers Gordon Fraser, Bernhard K. Aichernig, and Franz Wotawa \end{itemize} \subsubsection*{16:00 - 16:30 Coffee Break\\16:30 - 17:15 Discussion} \newpage \subsection{Programme of MOMPES } \subsubsection*{4th International Workshop on Model-based Methodologies for Pervasive and Embedded Software} \subsubsection*{Saturday, March 31, room: CP2-108} \subsubsection*{09:00 - 10:00 SESSION 1} \begin{description} \item[Opening and Welcome Session ]\item[Invited Talk ]\ \begin{itemize} \item On the Applicability Scope of Model Driven Engineering \\ \sp Jean B\'ezivin \end{itemize} \end{description} \subsubsection*{10:00 - 10:40 SESSION 2} \begin{description} \item[Pervasive Systems ]\ \begin{itemize} \item Towards a Model-Driven Approach for Ontology-Based Context-Aware Application Development: A Case Study \\ \sp Nektarios Georgalas, Shumao Ou, Manooch Azmoodeh, Kun Yang \item Tool Support for Model Driven Development of Pervasive Systems \\ \sp Carlos Cetina, Estefan\'{\i}a Serral, Javier Mu\~noz, Vicente Pelechano \end{itemize} \end{description} \subsubsection*{10:40 - 11:00 Coffee Break} \subsubsection*{11:00 - 11:40 SESSION 3} \begin{description} \item[Modelling Approaches ]\ \begin{itemize} \item A Generic Execution Framework for Models of Computation \\ \sp C\'ecile Hardebolle, Fr\'ed\'eric Boulanger, Dominique Marcadet, Guy Vidal-Naquet \item UML Profile for eXtreme Modeling Interactive Systems \\ \sp Alberto Rodrigues da Silva, Jo\~ao Saraiva, Rui Silva, Carlos Martins \end{itemize} \end{description} \subsubsection*{11:40 - 12:20 SESSION 4} \begin{description} \item[Formal Approaches (Chair: Ridha Khedri) ]\ \begin{itemize} \item Model-Driven Consistency Checking of Behavioural Specifications \\ \sp Bas Graaf, Arie van Deursen \item Challenges when using Model Driven Architecture in the Development of Safety Critical Software \\ \sp Philippa Conmy, Richard F. Paige \end{itemize} \end{description} \subsubsection*{12:30 - 14:30 Lunch} \subsubsection*{14:30 - 15:15 SESSION 5} \begin{description} \item[Invited Talk ]\ \begin{itemize} \item Executable Use Cases: a Supplement to Model-Driven Development? \\ \sp Jens B. J{\o}rgensen \end{itemize} \end{description} \subsubsection*{15:15 - 15:55 SESSION 6} \begin{description} \item[Software Product Lines ]\ \begin{itemize} \item Adopting Computational Independent Models for Derivation of Architectural Requirements of Software Product Lines \\ \sp Alexandre Bragan\c{c}a, Ricardo J. Machado \item Model-driven Development of Particle System Families \\ \sp Michalis Anastasopoulos, Andr\'as Balogh \end{itemize} \end{description} \subsubsection*{15:55 - 16:15 Coffee Break} \subsubsection*{16:15 - 16:55 SESSION 7} \begin{description} \item[Session on Embedded Systems (Chair: Lu\'{\i}s Gomes) ]\ \begin{itemize} \item ModES: Embedded Systems Design Methodology and Tools based on MDE \\ \sp Francisco Assis M. do Nascimento, M\árcio F. S. Oliveira, Fl\'avio Rech Wagner \item Designing a Unified Process for Embedded Systems \\ \sp Elvinia Riccobene, Patrizia Scandurra, Alberto Rosti, Sara Bocchio \end{itemize} \end{description} \subsubsection*{16:55 - 17:10 Closing Session} \newpage \subsection{Programme of OpenCert } \subsubsection*{Foundations and Techniques for Open Source Software Certification} \subsubsection*{Saturday, March 31, room: CP2-110} \subsubsection*{09:00 - 10:30 SESSION 1} \begin{itemize} \item Aspects of OSS Certification \\ \sp B. Aichernig, TU Graz, Austria \item Towards a Quality Model for OSS \\ \sp S.A. Shaikh \& A. Cerone, UNU-IIST, Macao \end{itemize} \subsubsection*{10:30 - 11:00 Coffee Break} \subsubsection*{11:00 - 12:30 SESSION 2} \begin{itemize} \item A System to Understand Programs Written in C Language by Code Annotation \\ \sp 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 \\ \sp N. Rodrigues, L. Barbosa, J.N. Oliveira Univ. Minho, Portugal \end{itemize} \subsubsection*{12:30 - 14:00 Lunch} \subsubsection*{14:00 - 15:30 SESSION 3} \begin{itemize} \item Linux Certification \\ \sp A.K. Petrenko, ISPRAS, Russia \item OSS Operating Systems for Critical Avionics Infrastructure: A survey on quality and security certification \\ \sp D. von Oheimb, Siemens, Germany \end{itemize} \subsubsection*{15:30 - 16:00 Coffee Break} \subsubsection*{16:00 - 18:30 SESSION 4} \begin{itemize} \item Position Talk on the OSS Certification Process \\ \sp P.T. Breuer \& S. Pickin, Univ. Carlos III Madrid, Spain \item A Perspective on OSS Certification \\ \sp J. Visser, SIG, The Netherlands \item Short Position Statements and Discussion \end{itemize} \newpage \subsection{Programme of QAPL } \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 ]\ \begin{itemize} \item Nondeterminism in Quantitative Analysis of Probabilistic Systems \\ \sp Roberto Segala (University of Verona, Italy) \end{itemize} \item[Paper Presentation: ]\ \begin{itemize} \item Keeping Secrets in Resource Aware Components \\ \sp Tom Chothia (CWI, The Netherlands), Jun Pang (University of Oldenburg, Germany) and Mohammad Torabi Dashti (CWI, The Netherlands) \end{itemize} \end{description} \subsubsection*{12:30 - 14:30 Lunch} \subsubsection*{14:30 - 16:00 SESSION 2} \begin{description} \item[Invited Talk ]\ \begin{itemize} \item Artificial Biochemistry \\ \sp Luca Cardelli (Microsoft Research, UK) \end{itemize} \item[Paper Presentation: ]\ \begin{itemize} \item Stochastic Concurrent Constraint Programming and Differential Equations \\ \sp Luca Bortolussi (University of Trieste, Italy) and Alberto Policriti (University of Udine, Italy) \end{itemize} \end{description} \subsubsection*{16:00 - 16:30 Coffee Break} \subsubsection*{16:30 - 18:00 SESSION 3} \begin{description} \item[Paper Presentations: ]\ \begin{itemize} \item On Probabilistic Techniques for Data Flow Analysis \\ \sp Alessandra Di Pierro, Chris Hankin and Herbert Wiklicky (Imperial College London, UK) \item Probabilistic Pi-Calculus and Event Structures \\ \sp Daniele Varacca (University of Paris 7, France) and Nobuko Yoshida (Imperial College London, UK) \item Probabilistic Barbed Congruence \\ \sp Yuxin Deng (Shanghai Jiao Tong University, China) and Wenjie Du (Shanghai Normal University, China) \end{itemize} \end{description} \subsubsection*{Sunday, March 25, room: CP2-105} \subsubsection*{09:30 - 10:30 SESSION 1} \begin{description} \item[Invited Talk ]\ \begin{itemize} \item Approximate Reasoning for Time and Probabilities \\ \sp Radha Jagadeesan (DePaul University, USA) \end{itemize} \end{description} \subsubsection*{10:30 - 11:00 Coffee Break} \subsubsection*{11:00 - 12:30 SESSION 2} \begin{description} \item[Paper Presentations: ]\ \begin{itemize} \item Modelling Multicast QoS Routing by using Best-Tree Search in And-or Graphs and Soft Constraint Logic Programming \\ \sp 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 \\ \sp Pedro Baltazar, Paulo Mateus (University of Lisbon, Portugal), Rajagopal Nagarajan and Nikolaos Papanikolaou (University of Warwick, UK) \end{itemize} \end{description} \subsubsection*{12:30 - 14:30 Lunch} \subsubsection*{14:30 - 16:00 SESSION 3} \begin{description} \item[Paper Presentations: ]\ \begin{itemize} \item Stochastic Modelling of Communication Protocols from Source Code \\ \sp Michael Smith (University of Edinburgh, UK) \item PEPA Queues: Capturing customer behaviour in queueing networks \\ \sp Ashok Argent-Katwala and Jeremy Bradley (Imperial College London, UK) \item A structural approach for modelling performance of systems using skeletons \\ \sp Gagarine Yaikhom, Murray Cole, Stephen Gilmore and Jane Hillston (University of Edinburgh, UK) \end{itemize} \end{description} \subsubsection*{16:00 - 16:30 Coffee Break} \subsubsection*{16:30 - 17:30 SESSION 4} \begin{description} \item[Short Paper Presentations: ]\ \begin{itemize} \item Distributed Liveness and Timers for Mobile Processes \\ \sp Martin Berger and Nobuko Yoshida (Imperial College London, UK) \item Stochastic Ambient Logic \\ \sp Maria Grazia Vigliotti (Imperial College London, UK) \end{itemize} \end{description} \subsubsection*{17:30 Steering Committee Meeting} \newpage \subsection{Programme of SC } \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 ]\ \begin{itemize} \item Composition by Anonymous Third Parties \\ \sp Farhad Arbab (CWI and Leiden University, NL) \end{itemize} \end{description} \subsubsection*{10:30 - 11:00 Coffee Break} \subsubsection*{11:00 - 12:30 SESSION 2} \begin{description} \item[Composition Contracts ]\ \begin{itemize} \item Defining Component Protocols with Service Composition: Illustration with the Kmelia Model \\ \sp Pascal Andr\'e, Gilles Ardourel, and Christian Attiogb\'e (University Of Nantes, F) \item Composite Contract Enforcement in Hierarchical Component Systems \\ \sp 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 \\ \sp Mario Bravetti and Gianluigi Zavattaro (University of Bologna, I) \end{itemize} \end{description} \subsubsection*{12:30 - 14:00 Lunch} \subsubsection*{14:00 - 16:00 SESSION 3} \begin{description} \item[Composition Design \& Analysis ]\ \begin{itemize} \item A Process-Algebraic Approach to Workflow Specification and Refinement \\ \sp Peter Wong and Jeremy Gibbons (University of Oxford, UK) \item Generic Feature-Based Software Composition \\ \sp Tijs Van der Storm (CWI, NL) \item Composition Management Interfaces for a predictable assembly \\ \sp Xabier Aretxandieta, Goiuria Sagardui (University of Mondragon, E), and Franck Barbier (Pau University, F)\} \item Error propagation analysis in composition of software services \\ \sp Vittorio Cortellessa (Universita' dell'Aquila, I) and Pasqualina Potena (Universit\'a ``G. D'Annunzio'', I) \end{itemize} \end{description} \subsubsection*{16:00 - 16:30 Coffee Break} \subsubsection*{16:30 - 18:00 SESSION 4} \begin{description} \item[Dynamic Composition ]\ \begin{itemize} \item Dynamically Adaptable Applications with iPOJO Service Components \\ \sp Clement Escoffier and Richard Hall (Grenoble University, F) \item Dynamic Contextual Service Ranking \\ \sp 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 \\ \sp Xingzhi Feng, Quanyuan Wu, Yan Jia, Bin Zhou, and Yi Ren (National University of Defense Technology, China) \end{itemize} \end{description} \subsubsection*{Sunday, March 25, room: CP2-101} \subsubsection*{09:30 - 10:30 SESSION 1} \begin{description} \item[Short Papers ]\ \begin{itemize} \item Measuring Reactability of Persistent Computing Systems \\ \sp Takumi Endo, Yuichi Goto, and Jingde Cheng (Saitama University, Japan) \item Requirements for applying aspect-oriented techniques in webservice composition languages \\ \sp Mathieu Braem and Niels Joncheere (Vrije Universiteit Brussel, B) \item Synthesizing Communication Middleware from Explicit Connectors in Component Based Distributed Architectures \\ \sp Dietmar Schreiner and Karl G\"oschka (Vienna University of Technology, A) \item Streamlining Feature-Oriented Designs \\ \sp Martin Kuhlemann, Sven Apel, and Thomas Leich (University of Magdeburg, D) \item Requirements for Reusable Aspect Deployment \\ \sp Bruno De Fraine and Mathieu Braem (Vrije Universiteit Brussel, B) \end{itemize} \end{description} \subsubsection*{10:30 - 11:00 Coffee Break} \subsubsection*{11:00 - 12:30 SESSION 2} \begin{description} \item[Aspect-Oriented Programming ]\ \begin{itemize} \item Aspect-Oriented Programming: Selecting and Exposing Object Paths \\ \sp Mohammed Al-Mansari, Stefan Hanenberg, and Rainer Unland (University of Duisburg-Essen, D) \item Debugging Aspect-Enabled Programs \\ \sp 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 \\ \sp Wasif Gilani and Fabian Scheler (Erlangen University, D) \end{itemize} \end{description} \subsubsection*{12:30 - 14:00 Lunch} \subsubsection*{14:00 - 16:00 SESSION 3} \begin{description} \item[Structural Composition ]\ \begin{itemize} \item Patterns of Component Evolution \\ \sp 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 \\ \sp Imed Hammouda and Kai Koskimies (Tampere University of Technology, FI) \item Composite Connectors for Composing Software Components \\ \sp Kung-Kiu Lau, Ling Ling, Vladyslav Ukis, and Perla Velasco (The University of Manchester, UK) \end{itemize} \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} \newpage \subsection{Programme of SLA\texttt{++}P } \subsubsection*{Model-driven High-level Programming of Embedded Systems} \subsubsection*{Saturday, March 31, room: CP2-105} \subsubsection*{09:00 - 10:30 SESSION 1} \begin{itemize} \item Welcome and Opening \item (Invited Talk) \\ \sp Dr. Steven Miller, Senior Principal Engineer in the Advanced Technology Center of Rockwell Collins, USA \item A Model Checking Approach to Protocol Conversion \\ \sp R.Sinha, P.S.Roop, S.Basu \end{itemize} \subsubsection*{10:30 - 11:00 Coffee Break} \subsubsection*{11:00 - 12:30 SESSION 2} \begin{itemize} \item Worst Case Reaction Time Analysis of Concurrent Reactive Programs \\ \sp M.Boldt, C.Traulsen, R.von Hanxleden \item Executable Specifications for Real-Time Distributed Systems \\ \sp A.Ray, R.Cleaveland \item (Short discussion) SYNCHRON'07 and SLAP'08 \end{itemize} \subsubsection*{12:30 - 14:00 Lunch} \subsubsection*{14:00 - 15:30 SESSION 3} \begin{itemize} \item Gotos in Esterel \\ \sp O.Tardieu, S.A.Edwards \item Specifying and executing reactive scenarios with Lutin \\ \sp P.Raymond, Y.Roux, E.Jahier \item Modifying Contracts with Larissa Aspects \\ \sp D.Stauch \end{itemize} \subsubsection*{15:30 - 16:00 Coffee Break} \subsubsection*{16:00 - 18:30 SESSION 4} \begin{itemize} \item Lustre as a System Modeling Language: Lussensor, a Case-Study with Sensor Networks \\ \sp F.Maraninchi, L.Samper, K.Baradon, A.Vasseur Madrid, Spain \item Mutation analysis for LUSTRE programs \\ \sp L.du Bousquet \item Extending Lustre with Timeout Automata \\ \sp J.Gao, M.Whalen, E.Van Wyk \end{itemize} \newpage \subsection{Programme of Termgraph } \subsubsection*{4th International Workshop on Computing with Terms and Graphs} \subsubsection*{Saturday, March 31, room: CP2-104} \subsubsection*{09:20 - 10:30 SESSION 1} \textbf{Welcome} \begin{itemize} \item An Algebra for Directed Bigraphs \\ \sp D. Grohmann and M. Miculan \item Modeling and Verifying Graph Transformations in Proof Assistants \\ \sp M. Strecker \end{itemize} \subsubsection*{10:30 - 11:00 Coffee Break} \subsubsection*{11:00 - 12:30 SESSION 2} \begin{itemize} \item Intensional properties of polygraphs \\ \sp G. Bonfante and Y. Guiraud \item Term-graph rewriting in TOM with relative positions \\ \sp E. Balland and P. Brauner \item Deduction Graphs with Universal Quantification \\ \sp H. Geuvers and I. Loeb \end{itemize} \subsubsection*{12:30 - 14:00 Lunch} \subsubsection*{14:00 - 16:00 SESSION 3} \begin{itemize} \item Rewritings for Polarized Mutiplicative and Exponential Proof Structures \\ \sp C. Fouquere and V. Mogbil \item Hard Combinators \\ \sp D. Bechet and S. Lippi \item Universal Boolean Systems \\ \sp D. Bechet and S. Lippi \item Interaction Nets with Nested Pattern Matching \\ \sp S. Sato and A. Hussan \item Sub-lambda-calculi, classified \\ \sp F-R. Sinot \end{itemize} \newpage \subsection{Programme of WITS } \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 ]\ \begin{itemize} \item Riccardo Focardi (University of Venice) \end{itemize} \item[Invited Talk ]\ \begin{itemize} \item On the use of formal models for proving cryptographic security notions \\ \sp V\'eronique Cortier \end{itemize} \end{description} \subsubsection*{10:30 - 11:00 Coffee Break} \subsubsection*{11:00 - 12:30 SESSION 2} \begin{description} \item[Computational Security ]\ \begin{itemize} \item Computationally Sound Analysis of Protocols using Bilinear Pairings \\ \sp Laurent Mazare \item On the Role of Scheduling in Simulation-Based Security \\ \sp Ran Canetti, Ling Cheung, Nancy Lynch and Olivier Pereira \item Inductive Trace Properties Imply Computational Security \\ \sp Arnab Roy, Anupam Datta, Ante Derek and John Mitchell \end{itemize} \end{description} \subsubsection*{12:30 - 14:00 Lunch} \subsubsection*{15:00 - 16:00 SESSION 3} \begin{description} \item[Information Flow ]\ \begin{itemize} \item On information flow and refinement-closure \\ \sp Gavin Lowe \item Nondeduciblity on strategies in the temporal logic of knowledge \\ \sp Catalin Dima and Constantin Enea \end{itemize} \end{description} \subsubsection*{16:00 - 16:30 Coffee Break} \subsubsection*{16:30 - 17:30 SESSION 4} \begin{description} \item[Static Analysis of Authentication ]\ \begin{itemize} \item Detecting Replay Attacks by Freshness Annotations \\ \sp Han Gao, Pierpaolo Degano, Chiara Bodei and Hanne Riis Nielson \item A Calculus of Challanges and Responses \\ \sp Michael Backes, Agostino Cortesi, Riccardo Focardi and Matteo Maffei \end{itemize} \end{description} \subsubsection*{Sunday, March 25, room: CP2-102} \subsubsection*{09:30 - 10:30 SESSION 1} \begin{description} \item[Invited Talk ]\ \begin{itemize} \item Certified access control on mobile interactive devices \\ \sp Thomas Jensen (Saitama University, Japan) \end{itemize} \end{description} \subsubsection*{10:30 - 11:00 Coffee Break} \subsubsection*{11:00 - 12:30 SESSION 2} \begin{description} \item[New Models for Security Protocols ]\ \begin{itemize} \item On the Specification of Secure Channels \\ \sp Christopher Dilloway and Gavin Lowe \item Causality-based Abstraction of Multiplicity in Security Protocols \\ \sp Michael Backes, Agostino Cortesi and Matteo Maffei \item Skeletons and the Shapes of Bundles \\ \sp Joshua Guttman, Shaddin Doghmi and F. Javier Thayer \end{itemize} \end{description} \subsubsection*{12:30 - 14:00 Lunch} \subsubsection*{15:00 - 16:00 SESSION 3} \begin{description} \item[Protocol Verification ]\ \begin{itemize} \item Verifying an implementation of SSH \\ \sp Erik Poll and Aleksy Schubert \item Partial Order Reduction for Branching Security Protocols \\ \sp Wan Fokkink, Mohammad Torabi Dashti and Anton Wijs \end{itemize} \end{description} \subsubsection*{16:00 - 16:30 Coffee Break} \subsubsection*{16:30 - 17:30 IFIP WG 1.7 Business Meeting} \newpage \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} \subsection{Program Transformation with Stratego/XT} \textbf{Saturday, March 24, 9:00 -- 12:30, room: CP2 106} 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} \subsection{Beyond the Generators: Practical Techniques for Real-World Software Generation} \textbf{Saturday, March 24, 14:00 -- 18:00, 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} \subsection{Mobility, Ubiquity, and Security} \textbf{Sunday, April 1, full day, room: 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. \subsubsection*{Programme} \begin{itemize} \item 9:00 - 9:45 PCC scenarios and platform (Gilles Barthe) \item 9:45 - 10:30 Type systems I: Secure information flow (David Pichardie)\\ \item 10:30 - 11:00 break\\ \item 11:00 - 11:45 Type systems II: Resource control (David Aspinall) \item 11:45 - 12:30 Type systems III: Ownership (Peter Müller)\\ \item 12:30 - 14:00 lunch break\\ \item 14:00 - 14:45 Mobius logics (Lennart Beringer) \item 14:45 - 15:30 Mobius tool suite (Joe Kiniry)\\ \item 15:30 - 16:00 break\\ \item 16:00 - 16:45 Perspectives (Gilles Barthe) \item 16:45 - 17:30 Discussion (Peter Müller)\\ \item 19:00 Tutorial Dinner (Gilles Barthe) \end{itemize} %\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} \newpage \section{Social Programme} \subsubsection*{Saturday, March 24: IFIP WG 1.3 Dinner (by invitation)} 18:30 Shuttle departure from University Campus, Gualtar IFIP WG1.3 Dinner at Pousada Santa Maria de Bouro \subsubsection*{Sunday, March 25: Joint Workshops Pre-Conference Dinner (tickets needed)} 18:45 Shuttle departure from University Campus, Gualtar Workshops Dinner at Bom Jesus \subsubsection*{Monday, March 26: Welcome Reception (free admittance)} 19:00 Location: Largo do Paço (city centre) Welcome Reception at University Rectorate building \subsubsection*{ Tuesday, March 27: 10th Anniversary Celebration (free admittance)} 19:00-20:30 Cocktail/Buffet at Theatro Circo 20:30-22:00 Tales of ETAPS past There will be very brief talks by five people from among those who have been involved in ETAPS over the years. They will speak in this order: \begin{itemize} \item Hartmut Ehrig \item Reinhard Wilhelm \item Don Sannella \item Jose Fiadeiro \item Perdita Stevens \end{itemize} Afterwards, there will be an informal panel giving anyone present an opportunity to ask questions of the speakers. 22:00-23:00 Anniversary Cake + 10 years Port Wine + Fado Concert \subsubsection*{Wednesday, March 28: Conference Banquet (tickets needed)} 19:00 Shuttle departure from Theatro Circo Conference banquet at Paço dos Duques, Guimarães \subsubsection*{Saturday, March 31: Joint Workshops Post-Conference Dinner (tickets needed)} 18:45 Shuttle departure from University Campus, Gualtar Workshops Dinner at Pousada Santa Maria de Bouro, Amares \newpage \section{Sponsors} We wish to thank the following sponsors and partners for their contribution to ETAPS 2007. \begin{description} \item[Associations and Research Centers]: \begin{itemize} \item European Association for Theoretical Computer Science \item European Association for Programming Languages and Systems \item European Association of Software Science and Technology \item Minho University, Portugal \item Centro de Ciências e Tecnologias de Computação \item Fundação para Ciência e Tecnologia \end{itemize} \item[Industrial Sponsors]: \begin{itemize} \item Enabler Wipro \item Cisco Systems, Inc. \item Multicert %\item Unicre \end{itemize} \item[Partners]: \begin{itemize} \item Câmara Municipal de Braga \item TAP Portugal \item Edigma \item ParadigmaXis \item Megatrónica \end{itemize} \mbox{} \newpage \mbox{} \newpage \newpage \thispagestyle{empty} %\includepdf[fitpaper=true]{spon.pdf} \mbox{}\hspace{-1cm}\includegraphics[width=.95\textwidth]{spon.png} \end{description} \end{document}