[Prev][Next][Index][Thread]
AMAST'96 Preliminary Program
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
[With apologies if you get this announcement more than once. G. Scollo]
-----------------------------------------------------------------------
o This announcement is also available via WWW or FTP, resp. at URL:
WWW : http://www.cs.utwente.nl/data/amast/amast96/PrelProg.txt
FTP : ftp://ftp.cs.utwente.nl/pub/doc/amast/amast96/PrelProg.txt
o The registration forms will be sent soon.
o 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
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
UniversitaB
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 fB
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 UniversitB
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 UniversitB
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