======================================================================= [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 AND SOFTWARE TECHNOLOGY AMAST '96 ******************************************* ********************************************* July 1-5, 1996 Munich, Germany Sponsored by Deutsche Forschungsgemeinschaft M"unchener Universit"atsgesellschaft s d & m Siemens Organized by Ludwig-Maximilians-Universit"at M"unchen FINAL PROGRAMME, REGISTRATION, ACCOMMODATION, and TRAVEL INFORMATION ********************************************************* FINAL PROGRAMME ********************************************************* ---------------------- EDUCATION DAY ---------------------- 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 ------------------------- CONFERENCE SCHEDULE ------------------------- 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 Specifications 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 Specifications 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 Bisimulation 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 WEDNESDAY, JULY 3rd, 1996 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 ********************************************************* REGISTRATION ********************************************************* REGISTRATION FEES ================== 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!) REGISTRATION FORM: ================== Please type or print: ***************** AMAST'96 Registration form ******************** Last Name: First Name: Title: Affiliation: Street Address: City: Country: Phone: Fax: E-mail: 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: hennicke@informatik.uni-muenchen.de or by surface mail to: Prof. Martin Wirsing AMAST'96 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 ********************************************************* ACCOMMODATION ********************************************************* Below you find a list of appropriate hotels in several price categories. PLEASE BOOK THE REQUIRED ROOMS YOURSELF (AS EARLY AS POSSIBLE!) ********** GUEST HOUSES ***************** All prices inclusive breakfast. Excelsior 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. Steinberg 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. Lettl 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 Garden. Cosmopolitan 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"). Ariston Uns"oldstr. 10 Tel. +89/22 26 91 Fax 291 35 95 Prices: Single: 145 DM Double: 200 DM SPECIAL PRICE IF BOOKED BEFORE May 28: 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. ********************************************************* TRAVEL INFORMATION ********************************************************* 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). HOW TO REACH THE CONFERENCE SITE AND THE HOTELS: 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 "Marienplatz-Ostbahnhof". 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.).