Algebraic Methodology and Software Technology

1. Front Matter

   Pages I-XI

   PDF

2. Invited Papers

   1. From Specifications to Code in Casl

      • David Aspinall, Donald Sannella

      Pages 1-14

   2. Automata and Games for Synthesis

      • Igor Walukiewicz

      Pages 15-20

   3. Pragmatics of Modular SOS

      • Peter D. Mosses

      Pages 21-40

   4. Tool-Assisted Specification and Verification of the JavaCard Platform

      • Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa

      Pages 41-59

   5. Higher-Order Quantification and Proof Search*

      • Dale Miller

      Pages 60-75

   6. Algebraic Support for Service-Oriented Architecture

      • José Luiz Fiadeiro

      Pages 75-82

3. Regular Papers

   1. Fully Automatic Adaptation of Software Components Based on Semantic Specifications*

      • Christian Haack, Brian Howard, Allen Stoughton, Joe B. Wells

      Pages 83-98

   2. HasCasl: Towards Integrated Specification and Development of Functional Programs

      • Lutz Schröder, Till Mossakowski

      Pages 99-116

   3. Removing Redundant Arguments of Functions*

      • María Alpuente, Santiago Escobar, Salvador Lucas

      Pages 117-132

   4. A Class of Decidable Parametric Hybrid Systems

      • Michaël Adélaïde, Olivier Roux

      Pages 132-146

   5. Vacuity Checking in the Modal Mu-Calculus*

      • Yifei Dong, Beata Sarna-Starosta, C. R. Ramakrishnan, Scott A. Smolka

      Pages 147-162

   6. On Solving Temporal Logic Queries

      • Samuel Hornus, Philippe Schnoebelen

      Pages 163-177

   7. Modelling Concurrent Behaviours by Commutativity and Weak Causality Relations*

      • Guangyuan Guo, Ryszard Janicki

      Pages 178-191

   8. An Algebra of Non-safe Petri Boxes

      • Raymond Devillers, Hanna Klaudel, Maciej Koutny, Franck Pommereau

      Pages 192-207

   9. Refusal Simulation and Interactive Games

      • Irek Ulidowski

      Pages 208-223

   10. A Theory of May Testing for Asynchronous Calculi with Locality and No Name Matching

       • Prasannaa Thati, Reza Ziaei, Gul Agha

       Pages 223-239

   11. Equational Axioms for Probabilistic Bisimilarity

       • Luca Aceto, Zoltán Ésik, Anna Ingólfsdóttir

       Pages 239-254

   12. Bisimulation by Unification*

       • Paolo Baldan, Andrea Bracciali, Roberto Bruni

       Pages 254-270

   13. Transforming Processes to Check and Ensure Information Flow Security*

       • Annalisa Bossi, Riccardo Focardi, Carla Piazza, Sabina Rossi

       Pages 271-286

This volume contains the proceedings of AMAST 2002, the 9th International Conference on Algebraic Methodology and Software Technology, held during September 9–13, 2002, in Saint-Gilles-les-Bains, R´eunion Island, France. The major goal of the AMAST conferences is to promote research that may lead to setting software technology on a ?rm mathematical basis. This goal is achieved through a large international cooperation with contributions from both academia and industry. Developing a software technology on a mathematical basis p- duces software that is: (a) correct, and the correctness can be proved mathem- ically, (b) safe, so that it can be used in the implementation of critical systems, (c) portable, i. e. , independent of computing platforms and language generations, (d) evolutionary, i. e. , it is self-adaptable and evolves with the problem domain. All previous AMAST conferences, which were held in Iowa City (1989, 1991), Twente (1993), Montreal (1995), Munich (1996), Sydney (1997), Manaus (1999), and Iowa City (2000), made contributions to the AMAST goals by reporting and disseminating academic and industrial achievements within the AMAST area of interest. During these meetings, AMAST attracted an international following among researchers and practitioners interested in software technology, progr- ming methodology, and their algebraic, and logical foundations.

• Abstract State Machines
• Algebraic Methods
• Algebraic State Machines
• Formal Methods
• Formal Specification
• Formal Verification
• Java
• Mathematical Software Construction
• Process Algebras
• Software Design
• Software Development
• algebra
• formal method
• model checking
• verification

• LORIA - CNRS & INRIA, Campus Scientifique, Bâtiment LORIA, Vandoeuvre-lès-Nancy, France

  Hélène Kirchner

• LORIA - INRIA, Villers-lès-Nancy, France

  Christophe Ringeissen

Policies and ethics