PROGRAMME OF FOSSACS

Programme of FOSSACS

WEDNESDAY, 10 April

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 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 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 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

THURSDAY, 11 April

9.00
10.00 FOSSACS Invited Talk
Bruno Courcelle (Université Bordeaux, F)
Semantical Evaluations as Monadic Second-order Compatible Structure Transformations
Session chair: Mogens Nielsen

10.00
10.45 Coffee

10.45
12.45 FOSSACS
Infinite State Systems

Session chair: Julian Bradfield

Higher-order Pushdown Trees are Easy
Teodor Knapik, Damian Niwinski, Pawel Urzyczyn (Université de la Réunion, F and Warsaw University, PL)
Model-Checking Infinite Systems Generated by Ground Tree Rewriting
Christof Löding (Aachen University of Technology, D)
Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds
Petr Jancar, Antonin Kucera, Faron Moller, Zdenek Sawa (University of Ostrava, CZ, Masaryk University, CZ, University of Wales Swansea, UK)
Note on the Tableau Technique for Commutative Transition Systems
Jiri Srba (University of Aarhus, DK)

12.45
14.15 Lunch

14.15
15.15 SPIN Invited Talk
Ed Clarke (Carnegie Mellon University)
SAT-based Counterexample Guided Abstraction Refinement
Session chair:

15.15
16.00 Coffee

16.00
17.30 FOSSACS
Logic

Session chair: Antoine Petit

Model Checking Fixed Point Logic with Chop
Martin Lange, Colin Stirling (University of Edinburgh, UK)
Verifying Temporal Properties using Explicit Approximants: Completeness for Context-free Processes
Ulrich Schöpp, Alex Simpson (University of Edinburgh, UK)
A Calculus of Circular Proofs and its Categorical Semantics
Luigi Santocanale (University of Calgary, CA)

17.30
17.45 Short Break

17.45
18.45 FOSSACS
Message Sequence Charts

Session chair: Doron Peled

Bounded MSC Communication
Markus Lohrey, Anca Muscholl (Université Paris VII, F)
Generalised Regular MSC Languages
Benedikt Bollig, Martin Leucker, Thomas Noll (Aachen University of Technology, D)

20.00 nyd

FRIDAY, 12 April

9.00
10.00 CC
and SPIN Invited Talk

Session chair: Nigel Horspool

Abstract Interpretation: Theory and Practice
Patrick Cousot (ENS, Paris, F)

10.00
10.45 Coffee

10.45
12.45 FOSSACS
Semantics

Session chair: Peter Mosses

Varieties of Effects
Carsten Führmann (University of Birmingham, UK)
Notions of computation determine monads
Gordon Plotkin, John Power (University of Edinburgh, UK)
A First-Order One-Pass CPS Transformation
Olivier Danvy, Lasse R. Nielsen (University of Aarhus, DK)
The Informatic Derivative at a Compact Element
Keye Martin (Oxford University, UK)

12.45
14.15 Lunch

14.15
15.45 FOSSACS
Process Calculi

Session chair: Andy Gordon

Minimizing Transition Systems for Name Passing Calculi: A Co-algebraic Formulation
Gianluigi Ferrari, Ugo Montanari, Marco Pistore (Universitá di Pisa, I and ITC-IRST Trento, I)
Linearity and Bisimulation
Nobuko Yoshida, Kohei Honda, Martin Berger (University of Leicester, UK and University of London, UK)
On Compositional Reasoning in the Spi-Calculus
Michele Boreale and Daniele Gorla (Universitá di Firenze, I)

15.45
16.15 Coffee

16.15
17.45 FOSSACS
Time and Probability

Session chair: Pierpaolo Degano

Proving Correctness of Timed Concurrent Constraint Programs
F. de Boer, M. Gabbrielli, M.C. Meo (Universiteit Utrecht, NL, Universitá di Udine, I, Universitá di L'Aquila, I)
On Model Checking Durational Kripke Structures
F. Laroussinie, N. Markey, and Ph. Schnoebelen (ENS de Cachan, F)
The Demonic Product of Probabilistic Relations
Ernst-Erich Doberkat (University of Dortmund, D)

17.45
18.00 Closing Session

20.00 SPIN dinner

WEDNESDAY, 10 April
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	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	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	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
THURSDAY, 11 April
9.00 10.00	FOSSACS Invited Talk Bruno Courcelle (Université Bordeaux, F) Semantical Evaluations as Monadic Second-order Compatible Structure Transformations Session chair: Mogens Nielsen
10.00 10.45	Coffee
10.45 12.45	FOSSACS Infinite State Systems Session chair: Julian Bradfield Higher-order Pushdown Trees are Easy Teodor Knapik, Damian Niwinski, Pawel Urzyczyn (Université de la Réunion, F and Warsaw University, PL) Model-Checking Infinite Systems Generated by Ground Tree Rewriting Christof Löding (Aachen University of Technology, D) Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds Petr Jancar, Antonin Kucera, Faron Moller, Zdenek Sawa (University of Ostrava, CZ, Masaryk University, CZ, University of Wales Swansea, UK) Note on the Tableau Technique for Commutative Transition Systems Jiri Srba (University of Aarhus, DK)
12.45 14.15	Lunch
14.15 15.15	SPIN Invited Talk Ed Clarke (Carnegie Mellon University) SAT-based Counterexample Guided Abstraction Refinement Session chair:
15.15 16.00	Coffee
16.00 17.30	FOSSACS Logic Session chair: Antoine Petit Model Checking Fixed Point Logic with Chop Martin Lange, Colin Stirling (University of Edinburgh, UK) Verifying Temporal Properties using Explicit Approximants: Completeness for Context-free Processes Ulrich Schöpp, Alex Simpson (University of Edinburgh, UK) A Calculus of Circular Proofs and its Categorical Semantics Luigi Santocanale (University of Calgary, CA)
17.30 17.45	Short Break
17.45 18.45	FOSSACS Message Sequence Charts Session chair: Doron Peled Bounded MSC Communication Markus Lohrey, Anca Muscholl (Université Paris VII, F) Generalised Regular MSC Languages Benedikt Bollig, Martin Leucker, Thomas Noll (Aachen University of Technology, D)
20.00	nyd
FRIDAY, 12 April
9.00 10.00	CC and SPIN Invited Talk Session chair: Nigel Horspool Abstract Interpretation: Theory and Practice Patrick Cousot (ENS, Paris, F)
10.00 10.45	Coffee
10.45 12.45	FOSSACS Semantics Session chair: Peter Mosses Varieties of Effects Carsten Führmann (University of Birmingham, UK) Notions of computation determine monads Gordon Plotkin, John Power (University of Edinburgh, UK) A First-Order One-Pass CPS Transformation Olivier Danvy, Lasse R. Nielsen (University of Aarhus, DK) The Informatic Derivative at a Compact Element Keye Martin (Oxford University, UK)
12.45 14.15	Lunch
14.15 15.45	FOSSACS Process Calculi Session chair: Andy Gordon Minimizing Transition Systems for Name Passing Calculi: A Co-algebraic Formulation Gianluigi Ferrari, Ugo Montanari, Marco Pistore (Universitá di Pisa, I and ITC-IRST Trento, I) Linearity and Bisimulation Nobuko Yoshida, Kohei Honda, Martin Berger (University of Leicester, UK and University of London, UK) On Compositional Reasoning in the Spi-Calculus Michele Boreale and Daniele Gorla (Universitá di Firenze, I)
15.45 16.15	Coffee
16.15 17.45	FOSSACS Time and Probability Session chair: Pierpaolo Degano Proving Correctness of Timed Concurrent Constraint Programs F. de Boer, M. Gabbrielli, M.C. Meo (Universiteit Utrecht, NL, Universitá di Udine, I, Universitá di L'Aquila, I) On Model Checking Durational Kripke Structures F. Laroussinie, N. Markey, and Ph. Schnoebelen (ENS de Cachan, F) The Demonic Product of Probabilistic Relations Ernst-Erich Doberkat (University of Dortmund, D)
17.45 18.00	Closing Session
20.00	SPIN dinner