Programme of Wednesday, April 10

ETAPS Invited Talk
Daniel Jackson (MIT Lab for Computer Science)
Alloy: A New Technology for Software Modelling
Session chair:  Susanne Graf
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)

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)

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)


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)

ETAPS Invited Talk
Mary Shaw (Carnegie Mellon University)
What Makes Good Research in Software Engineering?
Session chair:  José Fiadeiro
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)

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)

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)

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)

Short Break
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)

(Buses leave on 19:30)