Algebraic Methodology and Software Technology : Proceedings of the 9th International Conference, AMAST 2002, Saint-Gilles-Les-Bains, Reunion Island, France, September 9-13, 2002, Proceedings

by Kirchner, Helene; Ringeissen, Christophe

• ISBN13: 9783540441441
• ISBN10: 3540441441
• Format: Paperback
• Copyright: 2002-09-01
• Publisher: Springer Verlag

Summary

This book constitutes the refereed proceedings of the 9th International Conference on Algebraic Methodology and Software Technology, AMAST 2002, held in Saint-Gilles-les-Bains, Reunion Island, France in September 2002.The 26 revised full papers presented together with 6 invited papers and 2 system descriptions were carefully reviewed and selected from 59 submissions. Among the topics covered are all current issues in formal methods related to algebraic approaches including abstract data types, process algebras, algebraic specification, semantic specification, model checking, mu-calculus, Petri box algebras, unification, verification of Java for smart cards, security, JML specification, and formal software development.

Table of Contents

Invited Papers
From Specifications to Code in Casl	p. 1
Automata and Games for Synthesis	p. 15
Pragmatics of Modular SOS	p. 21
Tool-Assisted Specification and Verification of the JavaCard Platform	p. 41
Higher-Order Quantification and Proof Search	p. 60
Algebraic Support for Service-Oriented Architecture	p. 75
Regular Papers
Fully Automatic Adaptation of Software Components Based on Semantic Specifications	p. 83
HasCasl: Towards Integrated Specification and Development of Functional Programs	p. 99
Removing Redundant Arguments of Functions	p. 117
A Class of Decidable Parametric Hybrid Systems	p. 132
Vacuity Checking in the Modal Mu-Calculus	p. 147
On Solving Temporal Logic Queries	p. 163
Modelling Concurrent Behaviours by Commutativity and Weak Causality Relations	p. 178
An Algebra of Non-safe Petri Boxes	p. 192
Refusal Simulation and Interactive Games	p. 208
A Theory of May Testing for Asynchronous Calculi with Locality and No Name Matching	p. 223
Equational Axioms for Probabilistic Bisimilarity	p. 239
Bisimulation by Unification	p. 254
Transforming Processes to Check and Ensure Information Flow Security	p. 271
On Bisimulations for the Spi Calculus	p. 287
Specifying and Verifying a Decimal Representation in Java for Smart Cards	p. 304
A Method for Secure Smartcard Applications	p. 319
Extending JML Specifications with Temporal Logic	p. 334
Algebraic Dynamic Programming	p. 349
Analyzing String Buffers in C	p. 365
A Foundation of Escape Analysis	p. 380
A Framework for Order-Sorted Algebra	p. 396
Guarded Transitions in Evolving Specifications	p. 411
Revisiting the Categorical Approach to Systems	p. 426
Proof Transformations for Evolutionary Formal Software Development..	p. 441
Sharing Objects by Read-Only References	p. 457
Class-Based versus Object-Based: A Denotational Comparison	p. 473
System Descriptions
BRAIN: Backward Reachability Analysis with Integers	p. 489
The Development Graph Manager Maya	p. 495
Author Index	p. 503
Table of Contents provided by Publisher. All Rights Reserved.