PROGRAMME OF WEDNESDAY

Programme of Wednesday, April 10

9.00
10.00 ETAPS Invited Talk
Daniel Jackson (MIT Lab for Computer Science)
Alloy: A New Technology for Software Modelling
Session chair: Susanne Graf

10.00
10.45 Coffee

10.45
12.45 TACAS
Model checking: logics and algorithms

Session chair: John Hatcliff

Exploring Very Large State Spaces Using Genetic Algorithms
Patrice Godefroid, Sarfraz Khurshid (Bell Labs & MIT, USA)
Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems
Radu Mateescu (INRIA Rhône-Alpes, F)
The ForSpec Temporal Logic: A New Temporal Property-Specification Language
R. Armoni, L. Fix, A. Flaisher, R. Gerth, B. Ginsburg, T. Kanza, A. Landver, S. Mador-Haim, E. Singerman, A. Tiemeyer, M.Y. Vardi, Y. Zbar (Rice University, USA, & Intel, USA/Israel)
Fine-Grained Conjunction Scheduling for Symbolic Reachablity Analysis
HoonSang Jin, Andreas Kuehlmann, Fabio Somenzi (Univ. of Colorado, Boulder & Cadence Berkeley Labs, USA)
FASE
Requirements Engineering

Session chair: Tiziana Margaria (Dortmund, Germany)

An Authoring Tool for Informal and Formal Requirements Specifications
Reiner Hähnle, Kristofer Johannisson, Aarne Ranta (Chalmer University of Technology, Gothenburg, Sweden)
Introducing Context-Based Constraints for Requirements Engineering
Felix Bübl (Technical University of Berlin, Germany)
Formal Requirements Engineering using Observer Models
Andreas Nonnengart, Georg Rock, Werner Stephan (German Research Centre for Artificial Intelligence, Saarbruecken, Germany)
Automatic Generation of Use Cases from Workflows: a Petri net based approach
Oscar López, Miguel A. Laguna, Francisco J. García (Technological Institute of Costa Rica, University of Valladolid, University of Salamanca, Spain)
ESOP
Distributed programs: verification and analysis

Session chair: Florence Maraninchi

Thread-Modular Verification For Shared-Memory Programs
Cormac Flanagan, Stephen Freund, Shaz Qadeer (Compaq Systems research Center, Palo Alto, USA)
Timing UDP: mechanized semantics for sockets, threads and failures
Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov (University of Cambridge, UK)
Finite-Control Mobile Ambients
Witold Charatonik, Andrew D. Gordon, Jean-Marc Talbot (Max-Plank Institut für Informatik, D and University of Wroclaw, Poland, Microsoft Research, UK, LIFL, F)
Dependency Analysis of Mobile Systems
Jérôme Feret (ENS, Paris, F)
FOSSACS
Specification

Session chair: Andrzej Tarlecki

On the Integration of Observability and Reachability Concepts
Michel Bidoit, Rolf Hennicker (CNRS & ENS de Cachan, F and Ludwig-Maximillians-Universität München, D)
Logics Admitting Final Semantics
Alexander Kurz (CWI Amsterdam, NL)
On Specification Logics for Algebra-Coalgebra Structures: Reconciling Reachability and Observability
Corina Cîrstea (Oxford University, UK)
Heterogeneous Development Graphs and Heterogeneous Borrowing
Till Mossakowski (University of Bremen, D)

12.45
14.15 Lunch

14.15
15.15 ETAPS Invited Talk
Mary Shaw (Carnegie Mellon University)
What Makes Good Research in Software Engineering?
Session chair: José Fiadeiro

15.15
16.00 Coffee

16.00
17.30 TACAS
Model checking and testing (3)

Session chair: Ed Brinksma

A Temporal Logic Based Theory of Test Coverage and Generation
Hyoung Seok Hong, Insup Lee, Oleg Sokolsky, Hasan Ural (Univ. Pennsylvania, USA & University of Ottawa, Canada)
Synthesizing Monitors for Safety Properties
Klaus Havelund, Grigore Rosu (NASA Ames Research Center, USA)
Adaptive Model Checking
Alex Groce, Doron Peled, Mihalis Yannakakis (Carnegie Mellon Univ., USA, Univ. of Texas, Austin, & Avaya Laboratories, USA)
FASE
Case tools

Session chair: Marie-Claude Gaudel (Orsay, France)

Meta-modeling Techniques Meet Web Application Design Tools
Luciano Baresi, Franca Garzotto, Luca Mainetti, Paolo Paolini (Politecnico di Milano, Italy)
Formal-Driven Conceptualization and Prototyping of Hypermedia Applications
Antonio Navarro, Baltasar Fernandez-Manjon, Alfredo Fernandez-Valmayor, Jose Luis Sierra (Universidad Complutense de Madrid, Spain)
CC
Tool Demonstrations

Session chair:

LISA: An Interactive Environment for Programming Language Development
Mernik Marjan (University of Maribor, Slovenia)
Generating an Interpreter with vmgen
M. Anton Ertl (Technical University of Vienna, Austria)
Compiler Construction using LOTOS NT
Frederic Lang (INRIA Rhone-Alpes, F)
FOSSACS
Semantics and Types

Session chair: Don Sanella

Verification for Java's Reentrant Multithreading Concept
Erika Ábrahám-Mumm, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen (Christian-Albrechts-University Kiel, D and Utrecht University, NL)
Efficient Type Matching
Somesh Jha, Jens Palsberg, Tian Zhao (University of Wisconsin, USA and Purdue University, USA)
A Semantic Basis for Local Reasoning
Hongseok Yang, Peter O'Hearn (KAIST, Korea and University of London, UK)

17.30
17.45 Short Break

17.45
18.45 TACAS
Tool demo (1 of 2)

Session chair: Matthew Dwyer

STG: A Symbolic Test Generation Tool
Duncan Clarke, Thierry Jéron, Vlad Rusu, Elena Zinovieva (IRISA/INRIA Rennes, F)

empty empty FOSSACS
Distributed Systems

Session chair: Fernando Orejas

Characterization of Families of Graphs in which Election is Possible
Emmanuel Godard and Yves Métivier (Université Bordeaux, F)
Conflict Detection and Resolution in Access Control Policy Specifications
Manuel Koch, Luigi V. Mancini, Francesco Parisi-Presicce (Freie Universität Berlin, D and Univ. di Roma La Sapienza, I)

20.00 ETAPS DINNER
(Buses leave on 19:30)

9.00 10.00	ETAPS Invited Talk Daniel Jackson (MIT Lab for Computer Science) Alloy: A New Technology for Software Modelling Session chair: Susanne Graf
10.00 10.45	Coffee
10.45 12.45	TACAS Model checking: logics and algorithms Session chair: John Hatcliff Exploring Very Large State Spaces Using Genetic Algorithms Patrice Godefroid, Sarfraz Khurshid (Bell Labs & MIT, USA) Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems Radu Mateescu (INRIA Rhône-Alpes, F) The ForSpec Temporal Logic: A New Temporal Property-Specification Language R. Armoni, L. Fix, A. Flaisher, R. Gerth, B. Ginsburg, T. Kanza, A. Landver, S. Mador-Haim, E. Singerman, A. Tiemeyer, M.Y. Vardi, Y. Zbar (Rice University, USA, & Intel, USA/Israel) Fine-Grained Conjunction Scheduling for Symbolic Reachablity Analysis HoonSang Jin, Andreas Kuehlmann, Fabio Somenzi (Univ. of Colorado, Boulder & Cadence Berkeley Labs, USA)	FASE Requirements Engineering Session chair: Tiziana Margaria (Dortmund, Germany) An Authoring Tool for Informal and Formal Requirements Specifications Reiner Hähnle, Kristofer Johannisson, Aarne Ranta (Chalmer University of Technology, Gothenburg, Sweden) Introducing Context-Based Constraints for Requirements Engineering Felix Bübl (Technical University of Berlin, Germany) Formal Requirements Engineering using Observer Models Andreas Nonnengart, Georg Rock, Werner Stephan (German Research Centre for Artificial Intelligence, Saarbruecken, Germany) Automatic Generation of Use Cases from Workflows: a Petri net based approach Oscar López, Miguel A. Laguna, Francisco J. García (Technological Institute of Costa Rica, University of Valladolid, University of Salamanca, Spain)	ESOP Distributed programs: verification and analysis Session chair: Florence Maraninchi Thread-Modular Verification For Shared-Memory Programs Cormac Flanagan, Stephen Freund, Shaz Qadeer (Compaq Systems research Center, Palo Alto, USA) Timing UDP: mechanized semantics for sockets, threads and failures Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov (University of Cambridge, UK) Finite-Control Mobile Ambients Witold Charatonik, Andrew D. Gordon, Jean-Marc Talbot (Max-Plank Institut für Informatik, D and University of Wroclaw, Poland, Microsoft Research, UK, LIFL, F) Dependency Analysis of Mobile Systems Jérôme Feret (ENS, Paris, F)	FOSSACS Specification Session chair: Andrzej Tarlecki On the Integration of Observability and Reachability Concepts Michel Bidoit, Rolf Hennicker (CNRS & ENS de Cachan, F and Ludwig-Maximillians-Universität München, D) Logics Admitting Final Semantics Alexander Kurz (CWI Amsterdam, NL) On Specification Logics for Algebra-Coalgebra Structures: Reconciling Reachability and Observability Corina Cîrstea (Oxford University, UK) Heterogeneous Development Graphs and Heterogeneous Borrowing Till Mossakowski (University of Bremen, D)
12.45 14.15	Lunch
14.15 15.15	ETAPS Invited Talk Mary Shaw (Carnegie Mellon University) What Makes Good Research in Software Engineering? Session chair: José Fiadeiro
15.15 16.00	Coffee
16.00 17.30	TACAS Model checking and testing (3) Session chair: Ed Brinksma A Temporal Logic Based Theory of Test Coverage and Generation Hyoung Seok Hong, Insup Lee, Oleg Sokolsky, Hasan Ural (Univ. Pennsylvania, USA & University of Ottawa, Canada) Synthesizing Monitors for Safety Properties Klaus Havelund, Grigore Rosu (NASA Ames Research Center, USA) Adaptive Model Checking Alex Groce, Doron Peled, Mihalis Yannakakis (Carnegie Mellon Univ., USA, Univ. of Texas, Austin, & Avaya Laboratories, USA)	FASE Case tools Session chair: Marie-Claude Gaudel (Orsay, France) Meta-modeling Techniques Meet Web Application Design Tools Luciano Baresi, Franca Garzotto, Luca Mainetti, Paolo Paolini (Politecnico di Milano, Italy) Formal-Driven Conceptualization and Prototyping of Hypermedia Applications Antonio Navarro, Baltasar Fernandez-Manjon, Alfredo Fernandez-Valmayor, Jose Luis Sierra (Universidad Complutense de Madrid, Spain)	CC Tool Demonstrations Session chair: LISA: An Interactive Environment for Programming Language Development Mernik Marjan (University of Maribor, Slovenia) Generating an Interpreter with vmgen M. Anton Ertl (Technical University of Vienna, Austria) Compiler Construction using LOTOS NT Frederic Lang (INRIA Rhone-Alpes, F)	FOSSACS Semantics and Types Session chair: Don Sanella Verification for Java's Reentrant Multithreading Concept Erika Ábrahám-Mumm, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen (Christian-Albrechts-University Kiel, D and Utrecht University, NL) Efficient Type Matching Somesh Jha, Jens Palsberg, Tian Zhao (University of Wisconsin, USA and Purdue University, USA) A Semantic Basis for Local Reasoning Hongseok Yang, Peter O'Hearn (KAIST, Korea and University of London, UK)
17.30 17.45	Short Break
17.45 18.45	TACAS Tool demo (1 of 2) Session chair: Matthew Dwyer STG: A Symbolic Test Generation Tool Duncan Clarke, Thierry Jéron, Vlad Rusu, Elena Zinovieva (IRISA/INRIA Rennes, F)	empty	empty	FOSSACS Distributed Systems Session chair: Fernando Orejas Characterization of Families of Graphs in which Election is Possible Emmanuel Godard and Yves Métivier (Université Bordeaux, F) Conflict Detection and Resolution in Access Control Policy Specifications Manuel Koch, Luigi V. Mancini, Francesco Parisi-Presicce (Freie Universität Berlin, D and Univ. di Roma La Sapienza, I)
20.00	ETAPS DINNER (Buses leave on 19:30)