AMAST'96: Call for Partecipation

[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

[With apologies if you get this announcement more than once. B.Reus]

A word-wide-web page containing information about the conference is
reachable by URL: http://www.pst.informatik.uni-muenchen.de/amast96 .
e-mail:  amast96-info@informatik.uni-muenchen.de


                       FIFTH INTERNATIONAL CONFERENCE ON                     

                              ALGEBRAIC METHODOLOGY


                               SOFTWARE TECHNOLOGY

                                   AMAST '96


                               July 1-5, 1996

                              Munich, Germany

			        Sponsored by
	             Deutsche Forschungsgemeinschaft
		   M"unchener Universit"atsgesellschaft
				  s d & m

			       Organized by
		 Ludwig-Maximilians-Universit"at M"unchen



                   FINAL PROGRAMME



MONDAY, JULY 1st, 1996

09.00-10.00    Registration

10.00-10.15    Opening

10.15-11.45    Invited Talks

	Industrial Trials of Formal Specification
	John Fitzgerald
	University Newcastle upon Tyne, UK

	Industrial Applications of ASF+SDF
	Arie van Deursen
	CWI Amsterdam, The Netherlands

	An Experience with MEC in a Real Industrial Project
	Andre Arnold
	Univ. Bordeaux, France

11.45-12.15    Discussion

12.15-13.45    Lunch

13.45-15.15    Invited Talks

	Applying Research Results in the Industrial Environment:
	The Case of the TRIO Specification Language
	Dino Mandrioli
	Politecnico di Milano, Italy

	Using Heterogeneous Formal Methods in Distributed
	Software Engineering Education
	Bernd Kr"amer
	Fern-Universit"at Hagen, Germany

	Introducing Formal Methods to Software Engineers
	Through OMG's CORBA Environment and Interface
	Definition Language
	Sriram Sankar
	Sun Microsystems Laboratories, USA

15.15-15.45    Discussion


TUESDAY, JULY 2nd, 1996

08.00-8.45    Registration

08.45-9.00    Opening

09:00-10:00   Invited Talk
                Classification Approach to Design
                Douglas Smith
                Kestrel Institute, Palo Alto, USA

10:00-10:15   Discussion

10:15-10:45   Coffee Break

10:45-12:15   Session 1: Theorem Proving
	        Semantic Foundations for Embedding HOL in Nuprl
                D. J. Howe
	        AT&T Bell Laboratories, Murray Hill

   	        Free Variable Tableaux for a Many Sorted Logic with Preorders
                A. Gavilanes, J. Leach, S. Nieva
	        Univ. Complutense Madrid

	        Automating Induction over Mutually Recursive Functions
	        D. Kapur and M. Subramaniam
                Univ. at Albany, New York

12:15-13:45   Lunch

13:45-15:15   Session 2: Algebraic Specification

                Pushouts of Order-Sorted Algebraic Specifications
                A. E. Haxthausen and F. Nickl
                Techn. Univ. of Denmark and sd&m, M"unchen

                A Formal Framework for Modules with State
                D. Ancona and E. Zucca
                Univ. di Genova

                Object-Oriented Implementation of Abstract Data Type
                R. Hennicker and C. Schmitz
                LMU M"unchen and Univ. T"ubingen

15:15-15:30   Coffee Break

15:30-16:30   	System Demo Presentations

	        SPECWARE: An Advanced Environment for the Formal Development 
                of Complex Software Systems
                R. Juellig, Y. Srinivas, J. Liu
                Kestrel Institute, Palo Alto

		ASSPEGIQUE: An Integrated Specification Environment Providing
 		Inter-Operability of Tools
		M. Bidoit*, C. Choppy**, F. Voisin***
		LIENS, Paris*, IRIN, Univ. de Nantes**,
		LRI, Univ. de Paris-Sud***

		Towards Integrating Algebraic Specification and Functional  
		Programming: the Opal System
		K. Didrich, C. Gerke, W. Grieskamp, C. Maeder, P. Pepper
		Techn. Univ. Berlin

		InterACT: An Interactive Theorem Prover for Algebraic
		R. Geisler, M. Klar, F. Cornelius
                Techn. Univ. Berlin

		A new Proof-Manager and Graphic Interface for the Larch Prover
		F. Voisin
                LRI, Univ. de Paris-Sud

		TERSE: A Visual Environment for Supporting Analysis,
		Verification and Transformation of Term Rewriting Systems
		N. Kawaguchi, T. Sakabe, Y. Inagaki
                Nagoya Univ.

16:30-16:45   Coffee Break

16:45-18:15   Session 3: Concurrent and Reactive Systems

                On the Completeness of the Equations for the Kleene Star in 
                Wan Fokkink
                Utrecht Univ.

                An Equational Axiomatization of Observation Congruence for   

                Prefix Iteration
                L. Aceto and A. Ingolfsdottir
                Alborg Univ.

                Finite Axiom Systems for Testing Preorder and
                De Simone Process Languages
                I. Ulidowski
                Kyoto Univ.

19:00	      Reception


08:30-09:30   Invited Talk

                Constructive Semantics of Esterel: From Theory to Practice
                Gerard Berry
                Centre de Math. Appl., Sophia Antipolis, France

09:30-09:45   Discussion

09:45-10:15   Coffee Break

10.15-12:15   Session 4: Program Verification

                Using Ghost Variables to Prove Refinement
                M. Marcus and A. Pnueli
                Weizmann Institute of Science, Rehovot

                Tracing the Origins of Verification Conditions
                R. Fraer	
                INRIA, Sophia Antipolis

                Preprocessing for Invariant Validation
                E. P. Gribomont
                Univ. of Lie`ge

                Formal Verification of SIGNAL Programs:
                Application to a Power Transformer Station Controller
                M. Le Borgne*, H. Marchand*, E. Rutten*, M. Samaan**
                IRISA/INRIA, Rennes*, EDF/DER, Chatou**

12:15-13:45   Lunch

13:45-14:45   Invited Talk

                The Discrete Time Toolbus
                J.A. Bergstra and P. Klint
                CWI Amsterdam, The Netherlands

14:45-15:00   Discussion

15:00-15:15   Coffee Break

15:15-16:15   System Demo Presentations

		The TOOLBUS Coordination Architecture
		P. Klint
                Univ. Amsterdam					

 		A Demonstration of ASD: The Action Semantic Description Tools
		A. van Deursen and P. D. Mosses 	
                CWI Amsterdam and Aarhus Univ.

		Using Occurrence and Evolving Algebras for the
		Specification of Language-Based Programming Tools
		Arnd Poetzsch-Heffter
                Techn. Univ. M"unchen		

		ECHIDNA: A System for Manipulating Explicit Choice
		Higher Dimensional Automata
		R. Buckland and M. Johnson
        	Macquarie Univ.
		Verification using PEP
		S. Melzer, S. Romer, J. Esparza
                Techn. Univ. M"unchen

		The FC2TOOLS Set
		A. Bouali, A. Ressouche, V. Roy, R. de Simone
                INRIA, Sophia-Antipolis & Ecole des Mines de Paris

16:15-16:30   Coffee Break

16:30-18:00   Session 5: Concurrent and Reactive Systems

                A Study on the Specification and Verification of
                Performance Properties
                Xiao Jun Chen*, F. Corradini**, R. Gorrieri***
                Univ. "La Sapienza", Roma*, Univ. of Sussex**,
                Univ. di Bologna***

                Symbolic Bisimulation for Timed Processes
                M. Boreale
                Istituto per L'Elaborazione dell'Informazione, Pisa

                Approximative Analysis by Process Algebra with
                Graded Spatial Actions
                Y. Isobe, Y. Sato, K. Ohmaki
                Electrotechnical Laboratory, Tsukuba

THURSDAY, JULY 4th, 1996

08:30-09:30   Invited Talk

                Boolean Formalism and Explanations
                Eric C. R. Hehner
                University of Toronto, Canada

09:30-09:45   Discussion

09:45-10:15   Coffee Break

10.15-11:45   Session 6: Logic Programming and Term Rewriting

                Proving Existential Termination of Normal Logic Programs
                M. Marchiori
	        Univ. Padova

                Programming in Lygon: An Overview
                J. Harland*, D. Pym**, M. Winikoff***
                Royal Melbourne Institute of Technology*,
                Univ. of London**, Univ. of Melbourne***

                Some Characteristics of Strong Innermost Normalization
                M. R. K. Krishna Rao
                Max-Planck-Institut f"ur Informatik, Saarbr"ucken

11.45-12.15   System Demo Presentations
                Programming in Lygon: A System Demonstration
		J. Harland*, D. Pym**, M. Winikoff***
                Royal Melbourne Institute of Technology*,
                Univ. of London**, Univ. of Melbourne***
                CtCoq: A System Presentation
		J. Bertot and Y. Bertot
                INRIA, Sophia-Antipolis		

		The TYPELAB Specification and Verification Environment
		F. W. von Henke, M. Luther, M. Strecker, M. Wagner
                Univ. Ulm							

12:15-13:45   Lunch

13:45-14:45   Invited Talk

                On the Emergence of Properties in Component-Based Systems
	        J. L. Fiadeiro
                University of Lisbon, Portugal

14:45-15:00   Discussion

15:00-15:15   Coffee Break

15:15-16:15   System Demo Presentations
                Incremental Formalization
		B. Steffen, T. Margaria, A. Classen, V. Braun
                Univ. Passau

		PROPLANE: A Specification Development Environment
		J. Souquieres and N. Levy
                Univ. de Nancy

		A Logic-Based Technology to Mechanize Software Components Reuse
		P. Parot
               	INRIA, Le Chesnay				

		TkGofer: A Functional GUI Library
		W. Schulte, T. Schwinn, T. Vullinghs
                Univ. Ulm

		ALPHA - A Class Library for a
		Metamodel based on Algebraic Graph Theory
 		S. Erdmann and I. Classen
                Techn. Univ. Berlin							 				

16:15-16:30   Coffee Break

16:30-18:00   Session 7: Algebraic and Logical Foundations

                Algebraic View Specification
                B. Paech
                Techn. Univ. M"unchen

                Towards Heterogeneous Formal Specifications
                G. Bernot, S. Coudert, P. Le Gall
                Univ. d'Evry

                A Categorical Characterization of Consistency Results
                C. Baier and M. Majster-Cederbaum
                Univ. Mannheim

20:00	      Conference Dinner

FRIDAY, JULY 5th, 1996

08:30-09:30   Invited Talk

                Algebraic Specification of Reactive Systems
                Manfred Broy
                Technische Universit"at M"unchen, Germany

09:30-09:45   Discussion

09:45-10:15   Coffee Break

10.15-11:45   Session 8: Concurrent and Reactive Systems

                A Model for Mobile Point-To-Point Data-Flow
	        Networks without Channel Sharing
                R. Grosu and K.Stolen
	        Techn. Univ. M"unchen

                Coalgebraic Specifications and Models of
                Deterministic Hybrid Systems
                B. Jacobs
                CWI Amsterdam

                A Bounded Retransmission Protocol for Large Data Packets
                J.F. Groote and J. van de Pol
                Utrecht Univ.

11.45-12.15   System Demo Presentations
                Resolution of Goals with the Functional and Logic Programming
                Language LPG: Impact of Abstract Interpretation
		D. Bert, K. Adi, R. Echahed
                IMAG-LSR, Grenoble									

		Combining Reductions and Computations in ReDuX
		R. B"undgen and W. Lauterbach
                Univ. T"ubingen

		Conditional Directed Narrowing
		S. Limet and P. Rety
                LIFO-Univ. d'Orleans				

12:15-12.30   Closing





Before May 15:          400 DM ^
After May 15:           450 DM ^
Education Day only:     150 DM *

^ includes a copy of the proceedings, all coffee breaks and lunches,
  reception and banquet,
* includes coffee breaks and lunch on July 1st.

Extra Banquet Ticket   : 100 DM
Extra Reception Ticket :  30 DM.

Payment must be in German currency, and can be made by cheque payable
to "Prof. Martin Wirsing" or by bank transfer to:

Bank:		  Bayerische Vereinsbank M"unchen		
Bank code:	  70 020 270
Account no:	  41 936 290
Account holder:	  Prof. Martin Wirsing
Intended use:	  AMAST96

Bank transfers must specify registrant's name. Please ask your bank to
arrange the transfer free of charges to the beneficiary.
(No credit cards can be accepted!)


Please type or print:

***************** AMAST'96 Registration form ********************

Last Name:
First Name:
Street Address:

Arrival date  :
Departure date:

Payment is made by
cheques:  yes/no
bank transfer: yes/no

Total amount:
Includes extra tickets for:


Mail completed form either by e-mail to:


or by surface mail to:

    Prof. Martin Wirsing
    Institut f"ur Informatik
    Ludwig-Maximilians-Universit"at M"unchen
Before April 15th:
    Leopoldstr. 11B,
    D-80802 M"unchen,
After April 15th:
    Oettingenstr. 67,
    D-80538 M"unchen


Below you find a list of appropriate hotels in several price categories.


********** GUEST HOUSES *****************

All prices inclusive breakfast.

Kaulbachstr. 85 (1st floor)
Tel. +89/34 82 13
Prices:   Single: >= 65 DM  Double: 114 DM
(all rooms without WC and without bath)
Location: Munich-Schwabing, 10-15 min walk to the conference building
across the English Garden.

Ohmstr. 9 (1st floor)
Tel. +89/33 10 11
Fax  +89/33 10 11
Prices:   Single: >= 69 DM  Double: 100 DM
(rooms with WC and bath available)
Location: Munich-Schwabing, 10-15 min walk to the conference building  
across the English Garden.
Note: If you are interested in this guest house then please contact first
Rolf Hennicker (hennicke@informatik.uni-muenchen.de) since a special price  
may be possible.

**************** HOTELS *********************

All prices inclusive breakfast (if not stated otherwise) and
all rooms with WC and shower/bath.

Amalienstr. 53
Tel. +89/286 69 70
Fax +89/28 66 97 97
Prices:   Single: >= 110 DM  Double: >= 175 DM
Location: A small hotel in the University area, between Schwabing and the  
center. 25 min walk to the conference building, mainly through the English  

Hohenzollernstr. 5
Tel. +89/38 38 10
Fax +89/38 38 11 11
Prices:   Single: 145 DM  Double: 185 DM
Location: A modern hotel in the middle of Schwabing. 20 min walk to the  
conference building, mainly through the English Garden. You can also take  
the bus no. 54 (direction "Ostbahnhof", stop "Tivolistrasse") or bus no. 154  
(direction "Bruno-Walter-Ring", stop "Tivolistrasse").

Uns"oldstr. 10
Tel. +89/22 26 91
Fax 291 35 95
Prices:   Single: 145 DM  Double: 200 DM
Single: 90 DM   Double: 140 DM
(The code word for the special price is AMAST; if there are any problems  
ask for Mrs. Griessner)
Location: A hotel of the sixties, in Munich-Lehel, close to the center. 20  
min walk to the conference building. You can also take the tramway no. 17  
(direction "Effnerplatz", stop "Tivolistrasse").

M"unchen Park Hilton
Am Tucherpark 7
Tel. +89/38 450
Prices:   Single: 299 DM  Double: 370 DM (both exclusive breakfast)
Location: A comfortable hotel at the border of the English Garden. 5-10 min  
walk to the conference building.


Munich offers good access by air, rail, and road. The new Munich  
International Airport has frequent flights to and from most major cities. By  
rail, the city offers easy access to the major European centers.

The area of Munich is well served by the "S-Bahn" and the city by  
underground. There are single tickets (to be bought for each trip) or stripe  
cards ("Streifenkarte") which are relatively cheaper when used for several  
trips. Using a stripe card one has to cancel two stripes for any trip within  
Munich-City and eight stripes for one trip from Munich airport to the city  
(or conversely).


If you arrive at the airport
then take the S-Bahn no. 8 to Munich-City.

If you arrive at the central station
then take an arbitrary S-Bahn that goes into the direction of  

Then, in any case, proceed as follows:

To the conference building:

	Leave the S-Bahn at "Isartor";
	Change to tramway no. 17 (direction "Effnerplatz");
	Get out at "Tivolistrasse";
	Then the conference building (Oettingenstrasse 67) is
	on the other side of the street;
	Conference room = no. 114.
	Note: The conference building is known to many
	people in Munich as the previous "Radio Free Europe"
	building. This may be helpful if you have any trouble.

To guest houses Excelsior and Steinberg
and to Hotel Cosmopolitan:

	Leave the S-Bahn at "Marienplatz";
	Change to the underground no. U3 or no. U6
	(direction "M"unchner Freiheit");
	Get out at "Giselastrasse".

To Hotel Lettl:

	Leave the S-Bahn at "Marienplatz";
	Change to the underground no. U3 or U6
	(direction "M"unchner Freiheit");
	Get out at "Universit"at", exit "Schellingstrasse".

To Hotel Ariston:

	Leave the S-Bahn at "Isartor";
	Change to tramway no. 17 (direction "Effnerplatz");
	Get out at "Nationalmuseum/Haus der Kunst";

	(If you are arrived at the central station then it's better
	to choose directly the underground no. U4
	(direction "Arabellapark") or U5 (direction
	"Neuperlach S"ud"). Leave the underground at "Lehel".)

To M"unchen Park Hilton:

	It's the best to choose a Taxi at some place in Munich-City.
	Alternatively, you can first to go to the conference building
	and then walk to the hotel (5-10 min.).