Please find enclosed the call for participation for TAPSOFT '97. This call and other information on TAPSOFT '97 is also accessible by WWW at http://www.lifl.fr/tapsoft97. Sincerely apologize if you receive more than one copy of this message. Marc Tommasi Lab. d'Informatique Fondamentale de Lille -- Bat. M3 -- Cite Scientifique Univ. de Lille 1 -- 59655 Villeneuve d'Ascq CEDEX -- FRANCE ====================================================================== TAPSOFT'97 -- CALL FOR PARTICIPATION April 14-18, 1997 -- Lille, FRANCE http://www.lifl.fr/tapsoft97 TAPSOFT'97 is the Seventh International Joint Conference on the Theory and Practice of Software Development. The TAPSOFT series was started in Berlin in 1985, on the initiative of Hartmut Ehrig and Christiane Floyd (among others). Since then it has been held biennially, in Pisa, Barcelona, Brighton, Orsay and Aarhus. The overall aim of TAPSOFT was formulated as: to bring together theoretical computer scientists and software engineers (researchers and practitioners) with a view to discussing how formal methods can usefully be applied in software development. TAPSOFT is traditionally composed of CAAP -- Colloquium on Trees in Algebra and Programming, and FASE -- Colloquium on Formal Approaches in Software Engineering. In recognition of the importance of support tools for practical use of formal approaches, TAPSOFT'97 will also have (at least) a session where TOOLS are demonstrated. The five first editions of CAAP were held in Lille, from 1976 to 1980. CAAP'97 will be the last one thus it comes back to Lille. In 1998, a new joint conference, ETAPS (European joint conferences on Theory and Practice of Software) will be held yearly in Spring. It is the successor of TAPSOFT and CAAP-ESOP-CC. ----------------------------------- CAAP ------------------------------------ Programme Committee: S. Abramsky (UK) A. Arnold (France) G. Ausiello (Italy) C. Boehm (Italy) M. Dauchet (chair, France) J. Diaz (Spain) H. Ehrig (Germany) P. Franchi Zannettacci (France) J.-P. Jouannaud (France) H. Kirchner (France) U. Montanari (Italy) M. Nielsen (Denmark) M. Nivat (France) J.-F. Perrot (France) J.-C. Raoult (France) S. Tison (France) CAAP cover a wide range of topics in theoretical computer science; contributions on the following topics are especially welcome: properties of discrete structures, the theory of formal languages, syntax and semantics of programming languages, algorithms and data-structures, logic and formal verification, theoretical problems arising in software development. --------------------------------- FASE -------------------------------------- Programme Committee: E. Astesiano (Italy) D. Basin (Germany) M. Bidoit (chair, France) E. Brinskma (The Netherlands) L. Cardelli (USA) A. Finkel (France) J. Fitzgerald (UK) P.G. Larsen (Denmark) T. Henzinger (USA) P. Klint (The Netherlands) P. Mosses (Denmark) F. Orejas (Spain) D. Sannella (UK) B. Steffen (Germany) M. Wirsing (Germany) This colloquium aims at being a forum where different formal approaches to problems of software specification, development, and verification are presented, compared, and discussed. Contributions on the following topics are especially welcome: -- formal concepts for software development, -- software development using formal methods, -- formal approaches for real-time and distributed systems, -- provably correct software and verification methods, -- reports on case studies of applications of formal methods, -- programming languages and type systems, -- tools and environments supporting formal approaches -- possibly in conjunction with demonstrations. --------------------------- INVITED SPEAKERS -------------------------------- E. Astesiano (Italy) : "Formalism and Method" J.-P. Jouannaud(France): "Membership Equational Logic" T. Maibaum (UK) : "Conservative Extensions, Interpretations between theories and all that" P. Mosses(Denmark) : "The Common Framework Initiative for Algebraic Specification and Development" W. Thomas(Germany) : "Automata on finite trees and partial orders" F. Vaandrager(NL) : "A theory of Testing for Times Automata" -------------------------- CONFERENCE INFORMATION --------------------------- Additional information, site information, maps, updates, visa, tourist info, reservation form, accomodation form etc. can be obtained on http://www.lifl.fr/tapsoft97/ ftp://ftp.lifl.fr/pub/tapsoft97 [EMAIL PROTECTED] TAPSOFT Steering Committee: -------------------------- A. Arnold, P. Degano, H. Ehrig, M.-C. Gaudel, T. Maibaum, U. Montanari, P.D. Mosses, M. Nivat, F. Orejas. TAPSOFT'97 Organizing Committee: ------------------------------- A.C. Caron (chair), Y. Andre, F. Bossut, J.L. Coquide, M. Dauchet, R. Gilleron, S. Tison, M. Tommasi. -------------------------- PRELIMINARY PROGRAMME ---------------------------- Monday 14 april, morning ------------------------ REGISTRATION INVITED LECTURE Automata on finite trees and partial orders. W. Thomas, Univ. Kiel CAAP-1 : Rewriting and Automata FASE-1 : Specifications --------------------------------------------------------------------- Logicality of Conditional Semantics of Architectural Rewrite Systems. Connectors. T. Yamada, Loria-Saenz J.L. Fiadeiro and A. Lopes J. Avenhaus A. Middeldorp Simulating Forward-Branching Protective Interface Systems with Constructor Systems. Specifications. B. Salinier R. Strandh G. Leavens J. Wing Reliable Generalized and Context Specifying Complex and Structured Dependent Commutation Relations. Systems with Evolving Algebras. I. Biermann B. Rozoy W. May Word into Tree Transducers with Bounded Difference. Y. Andre F. Bossut Monday 14 april, afternoon -------------------------- INVITED LECTURE A theory of Testing for Times Automata. F. Vaandrager, Univ. of Nijmegen CAAP-2 : Automata and Time FASE-2 : Real-Time and distributed systems ----------------------------------------------------------------------------- Generalized Quantitative Compositional Specification of Temporal Reasoning: Embedded Systems with Statecharts. An Automata Theoretic Approach. E.A. Emerson R.J. Trefler J. Phillips P. Scholz The Railroad Crossing Problem: Verification of Message Sequence Towards Semantics of Timed Charts via Template Matching. Algorithms and their Model- Checking in High-Level Languages. D. Beauquier A. Slissenko V. Levin D. Peled Model Checking through Symbolic Probabilistic Lossy Channel Reachability Graph. Systems. J.-M. Ilie K. Ajami P. Iyer M. Narasimha Optimal Implementation of Wait-Free Binary Relations. E. Goubault Tuesday 15 april, morning ------------------------- INVITED LECTURE Conservative Extensions, Interpretations between theories and all that. Tom Maibaum, Imperial College, London CAAP-3 : Termination FASE-3 : Types and their Applications ------------------------------------------------------------------------ Relative Undecidability in the Reactive Types. Termination Hierarchy of Single Rewrite Rules. A. Geser A. Middeldorp J-P. Talpin E. Ohlebush H. Zantema Termination Proofs using gpo A Type-Based Approach to Ordering Constraints. Program Security. T. Genet I. Gnaedig D. Volpano G. Smith Automatically Proving An applicative module calculus. Termination Where Simplification Orderings Fail. J. Courant (LIP, Lyon) T. Arts J. Giesl Generating Efficient, Terminating Logic Programs. J.C. Martin A. King Tuesday 15 april, afternoon --------------------------- Tools Demonstrations - 1 Typelab: An environment for modular program development. F.W. von Henke, M. Luther, M. Strecker TAS and IsaWin: Generic Interfaces for Transformational Program Development and Theorem Proving. Kolyang, Ch. Lueth, T. Meyer, B. Wolff Proving System Correctness with KIV. W. Reif, G. Schellhorn, K. Stenzel A new Proof-Manager and Graphic Interface for the Larch Prover. F. Voisin CAAP-4 : Bi-simulations and FASE-4 : Verification Pi-calculus --------------------------------------------------------------------- Modal Characterization of Weak A Comparison of Modular Bisimulation for Higher-order Verification Techniques. Processes. H.R. Andersen J. Staunstrup M. Baldamus J. Dingel N. Maretti Formats of Ordered SOS Rules A Compositional Proof of a with Silent Actions. Real-Time Mutual Exclusion Protocol. I. Ulidowski I. Phillips K.J. Kristoffersen F. Laroussinie K.G. Larsen P. Pettersson Wang Yi The Congruence Candidate Method Traces of I/O-Automata in for Giving Coinductive Isabelle/HOLCF. Characterizations of Observational Equivalences in Lambda-calculi. O. Mueller T. Nipkow M. Lenisa A Labelled Transition Systems for pi-epsilon-Calculus. F. Van Breugel Wednesday 16 april, morning --------------------------- INVITED LECTURE Membership Equational Logic. A. Bouhoula, Nancy and SRI-International, J.P. Jouannaud, Univ. Paris XI and SRI-International, and J. Meseguer, SRI-International CAAP-5 : Set Constraints FASE-5 : Semantics --------------------------------------------------------------------- Set Operations for Recurrent A Logic of Object-Oriented term Schematizations. Programs. A. Amaniss, M. Hermann, M. Abadi, K. Rustan D. Lugiez M. Leino Inclusion Constraints over Auxiliary Variables and Non-empty Sets of Trees. Recursive Procedures. M. Muller, J. Niehren A. Podelski T. Schreiber Grid Structure and Undecidable Locality based Linda: programming Constraint Theories. with explicit localities. F. Seynhaeve M. Tommasi R. De Nicola G. Ferrari R. Treinen R. Pugliese Wednesday 16 april, afternoon ----------------------------- Tools Demonstrations - 2 A Web-based Animator for Object Specifications in a Persistent Environment. M. Richters and M. Gogolla Publishing Formal Specifications in Z Notation on World Wide Web. L. Mikusiak, M. Adamy and T. Seidmann DOSFOP - A Documentation Tool for the Algebraic Programming Language OPAL. K. Didrich, T. Klein AG: A set of Maple packages for symbolic computing of automata and semigroups. P. Caron CAAP-6 : Complexity FASE-6 : Static Analysis --------------------------------------------------------------------- Parallel Polynomial Time A Syntactic Theory of Dynamic Computation and Higher Order Binding. Recurrence. D. Leivant J.Y. Marion L. Moreau On the Complexity of Function A Unified Framework for Pointer May-Alias Analysis. Binding-Time Analysis. R. Muth S. Debray P. Thiemann Maximum packing for biconnected A Typed Intermediate Language outerplanar graphs. for Flow-Directed Compilation. T. Kovac A. Lingas J.B. Wells A. Dimock R. Muller F. Turbak Synchronization of a line of identical processors at a given time. S. La Torre M. Napoli M. Parente Thursday 17 april, morning -------------------------- INVITED LECTURE Formalism and Method. E. Astesiano and G. Reggio, DISI, Universita di Genova CAAP-7 : Unification and Matching FASE-7 : Refinement -------------------------------------------------------------------- An algorithm for the solution Action Refinement as an of tree equations. Implementation Relation. S. Mantaci D. Micciancio A. Rensink R. Gorrieri E-Unification by Means of Tree Simulation-Refinement of Tuple Synchronized Grammars. Coalgebraic Specifications S. Limet P. Rety with Coinductive Correctness Proofs. B. Jacobs Linear interpolation for the higher order matching problem. A. Schubert Thursday 17 april, afternoon ---------------------------- SPECIAL PANEL DISCUSSION for the last TAPSOFT (and CAAP), before the first ETAPS Invited panelists C. Boehm, Univ. Roma, H. Ehrig, TU-Berlin Univ., M. Nivat, Univ Paris VII, Don Sannella, Univ. Edinburgh SOCIAL EVENT BANQUET Friday 18 april, morning ------------------------ INVITED LECTURE The Common Framework Initiative for Algebraic Specification and Development. Peter D. Mosses, BRICS, University of Aarhus CAAP-8 : Types FASE-8 : Applications of Formal Methods to Software Engineering -------------------------------------------------------------------------- A semantic Framework for COMPASS: A Comprehensible Functional Logic Programming with Assertion Method. Algebraic Polymorphic Types. S. Bonnier T. Heyer P. Arenas-Sanchez M. Rodriguez-Artalejo Subtyping Constraints for Using LOTOS Patterns to Characterize Incomplete Objects. Architectural Styles. V. Bono M. Bugliesi M. Heisel N. L\'evy M. Dezani-Ciancaglini L. Liquori Partializing Stone Spaces Automating Formal using SFP domains. Specification-Based Testing. F. Alessi P. Baldan M.R. Donat Furio Honsell Let-Polymorphism and Eager Type Schemes. C. Liang
