AMAST'2002 Preliminary Program

September 9-13, 2002

St. Gilles les Bains, Reunion Island, France

Monday, September 9

09:00-09:30, Welcome and Introduction

Hélène Kirchner, Teodor Knapik and Christophe Ringeissen

09:30-10:30, Invited Talk

Don Sannella:
From specifications to code in CASL

Break

11:00-12:30, Session 1

11:00	Fully Automatic Adaptation of Software Components Based on Semantic Specifications
	C.Haack, B.Howard, A.Stoughton, J.Wells
11:30	HASCASL: Towards Integrated Specification and Development of Functional Programs
	L.Schroeder, T.Mossakowski
12:00	Removing Redundant Arguments of Functions
	M.Alpuente, S.Escobar, S.Lucas

Lunch

14:00-15:00, Invited Talk

Igor Walukiewicz:
Automata and Games for Synthesis

Break

15:30-16:15, Session 2

15:30	A Class of Decidable Parametric Hybrid Systems
	M.Adelaide, O.Roux
16:00	BRAIN: Backward Reachability Analysis with INtegers (System description)
	T.Rybina, A.Voronkov

Break

16:30-17:30, Session 2'

16:30	Vacuity Checking in the Modal Mu-Calculus
	Y.Dong, B.Sarna-Starosta, CR.Ramakrishnan, S.Smolka
17:00	On Solving Temporal Logic Queries
	S.Hornus, P.Schnoebelen

09:00-10:00, Invited Talk

Peter Mosses:
Pragmatics of Modular SOS

Break

10:30-12:00, Session 3

10:30	Modelling Concurrent Behaviours by Commutativity and Weak Causality Relations
	G.Guo, R.Janicki
11:00	An Algebra of Non-safe Petri Boxes
	R.Devillers, H.Klaudel, M.Koutny, F.Pommereau
11:30	Refusal Simulation and Interactive Games
	I.Ulidowski

Lunch

14:00-15:30, Session 4

14:00	Theory of May Testing for Asynchronous Calculi with Locality and No Name Matching
	P.Thati, R.Ziaei, G.Agha
14:30	Equational Axioms for Probabilistic Bisimilarity
	L.Aceto, Z.Esik, A.Ingolfsdottir
15:00	Bisimulation by unification
	P.Baldan, A.Bracciali, R.Bruni

Break

16:00-17:00, Session 4'

16:00	Transforming processes to ensure and/or check Information Flow Security
	A.Bossi, R.Focardi, C.Piazza, S.Rossi
16:30	On Bisimulations for the Spi Calculus
	J.Borgstrom, U.Nestmann

Excursion Day (departure of the bus at 8:00)

19:30, Steering Committee Meeting

09:30-10:30, Invited Talk

Gilles Barthe:
Tool-Assisted Specification and Verification of the JavaCard Platform

Break

11:00-12:30, Session 5

11:00	Specifying and Verifying a Decimal Representation in Java for Smart Cards
	C.Breunesse, B.Jacobs, J.van den Berg
11:30	A Method for Secure Smartcard Applications
	D.Haneberg, W.Reif, K.Stenzel
12:00	Extending JML Specifications with Temporal Logic
	K.Trentelman, M.Huisman

Lunch

14:00-15:00, Invited Talk

Dale Miller:
Higher-order quantification and proof search

Break

15:30-17:00, Session 6

15:30	Algebraic Dynamic Programming
	R.Giegerich, C.Meyer
16:00	Analyzing String Buffers in C
	A.Simon, A.King
16:30	A Foundation of Escape Analysis
	P.Hill, F.Spoto

Conference Dinner (departure of the bus at 18:30)

09:00-10:00, Invited Talk

Jose Fiadeiro:
Algebraic Support for Service-Oriented Architecture

Break

10:30-12:00, Session 7

10:30	A Framework for Order-Sorted Algebra
	J.Stell
11:00	Guarded Transitions in Evolving Specifications
	D.Pavlovic, D.Smith
11:30	Revisiting the Categorical Approach to Systems
	A.Lopes, J.Fiadeiro

Lunch

14:30-15:15, Session 8

14:30	Proof Transformations for Evolutionary Formal Software Development
	A.Schairer, D.Hutter
15:00	The Development Graph Manager Maya (System description)
	S.Autexier, D.Hutter, T.Mossakowski, A.Schairer

Break

15:30-16:30, Session 8'

15:30	Sharing Objects by Read­only References
	M.Skoglund
16:00	Class­based versus Object­based: A Denotational Comparison
	B.Reus