********************************************* * ***************************************** * * * * * * * * * * * FIFTH INTERNATIONAL CONFERENCE ON * * * * * * * * * * * * ALGEBRAIC METHODOLOGY * * * * * * * * AND * * * * * * * * SOFTWARE TECHNOLOGY * * * * * * * * AMAST '96 * * * * * * * ***************************************** * ********************************************* July 1-5, 1996 Ludwig-Maximilians-Universit"at Munich, Germany. Preliminary Program @@@@@@@@@@@@@@@@@@@@@@@ @ @ @ EDUCATION DAY @ @ @ @@@@@@@@@@@@@@@@@@@@@@@ MONDAY, JULY 1st, 1996 10.00 - 18.00 An experience with MEC in a real industrial project Andre Arnold University of Bordeaux, France Industrial Applications of ASF+SDF Arie van Deursen Techn. Univ. Eindhoven, The Netherlands Industrial Trials of Formal Specification John Fitzgerald University Newcastle upon Tyne, UK Using Heterogeneous Formal Methods in Distributed Software Engineering Education Bernd Kramer Fern-Universitat Hagen, Germany Applying Research Results in the Industrial Environment: The Case of the TRIO Specification Language Dino Mandrioli Politecnico di Milano, Italy Introducing Formal Methods to Software Engineers Through OMG's CORBA Environment and Interface Definition Language Sriram Sankar Sun Microsystems Laboratories, USA @@@@@@@@@@@@@@@@@@@@@@@ @ @ @ 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, M. Subramaniam University 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 The Technical University of Denmark, Lyngby and sd&m, M"unchen A Formal Framework for Modules with State D. Ancona and E. Zucca Universita€ di Genova Object-Oriented Implementation of Abstract Data Type Specifications R. Hennicker and C. Schmitz Ludwig-Maximilians-Universit"at M"unchen and Universit"at 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** and F. Voisin*** LIENS, C.N.R.S. & Ecole Normale Supe'rieure,Paris*, IRIN, Universite' de Nantes & Ecole Centrale, Nantes**, LRI, C.N.R.S. & Universite' de Paris-Sud, Orsay*** Towards Integrating Algebraic Specification and Functional Programming: the Opal System K. Didrich, C. Gerke, W. Grieskamp, C. Maeder, P. Pepper Technische Universit"at Berlin InterACT: An Interactive Theorem Prover for Algebraic Specifications R. Geisler, M. Klar, F. Cornelius Technische Universit"at Berlin A new Proof-Manager and Graphic Interface for the Larch Prover F. Voisin LRI, C.N.R.S. & Universite' de Paris-Sud, Orsay TERSE: A Visual Environment for Supporting Analysis, Verification and Transformation of Term Rewriting Systems N. Kawaguchi, T. Sakabe, Y. Inagaki Nagoya University 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 University An Equational Axiomatization of Observation Congruence for Prefix Iteration L. Aceto and A. Ingolfsdottir Alborg University Finite Axiom Systems for Testing Preorder and De Simone Process Languages I. Ulidowski Kyoto University 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, France Preprocessing for Invariant Validation E. P. Gribomont University 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, EP, dept. CCC, 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 University of Amsterdam A Demonstration of ASD: The Action Semantic Description Tools A. van Deursen and P. D. Mosses Eindhoven University of Technology and Aarhus University Using Occurrence and Evolving Algebras for the Specification of Language-Based Programming Tools Arnd Poetzsch-Heffter Technische Universit"at M"unchen ECHIDNA: A System for Manipulating Explicit Choice Higher Dimensional Automata R. Buckland and M. Johnson Macquarie University Verification using PEP S. Melzer, S. Romer, J. Esparza Technische Universit"at 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*** Universita` "La Sapienza", Roma*, University of Sussex, Brighton**, Universita` di Bologna*** Symbolic Bisimulation for Timed Processes M. Boreale Istituto per L'Elaborazione dell'Informazione-C.N.R.,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 University of Padova Programming in Lygon: An Overview J. Harland*, D. Pym**, M. Winikoff*** Royal Melbourne Institute of Technology, Melbourne*, University of London**, University of Melbourne*** Some Characteristics of Strong Innermost Normalization M. R. K. Krishna Rao Max-Planck-Institut f€r 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, Melbourne*, University of London**, University 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 Universit"at 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 Universit"at Passau PROPLANE: A Specification Development Environment Jeanine Souquieres and Nicole Levy Universite' de Nancy A Logic-Based Technology to Mechanize Software Components Reuse Patrick Parot INRIA Le Chesnay TkGofer: A Functional GUI Library W. Schulte, T. Schwinn, T. Vullinghs Universit"at Ulm Object-oriented Design of a Class Library for a Metamodel based on Algebraic Graph Theory S. Erdmann and I. Classen Technische Universit"at Berlin 16:15-16:30 Coffee Break 16:30-18:00 Session 7: Algebraic and Logical Foundations Algebraic View Specification B. Paech Technische Universit€t M"unchen Towards Heterogeneous Formal Specifications G. Bernot, S. Coudert, P. Le Gall Universite' d'Evry A Categorical Characterization of Consistency Results C. Baier and M. Majster-Cederbaum Universit"at Mannheim FRIDAY, JULY 5th, 1996 @@@@@@@@@@@@@@@@@@@@@@@@ 08:30-09:30 Invited Talk Algebraic Specification of Reactive Systems Manfred Broy Technische Universit€t 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 Technische Universit"at 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 University 11.45-12.15 System Demo Presentations Resolution of Goals with the Functional and Logic programming Language LPG: Impact of Abstract Interpretation Didier Bert, Kamel Adi, Rachid Echahed IMAG-LSR,CNRS, Grenoble Combining Reductions and Computations in ReDuX R. B"undgen and W. Lauterbach Universit"at T"ubingen Conditional Directed Narrowing S. Limet and P. Rety LIFO-Universite' d'Orleans 12:15-13:45 Lunch --------------------------------------------------------------------------- The registration forms will be sent soon. 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