Algebraic Methodology and Software Technology: 10th International Conference, AMAST 2004, Stirling, Scotland, UK, July 12-16, 2004, Proceedings (Lecture Notes in Computer Science, 3116)

This book constitutes the refereed proceedings of the 10th International Conference on Algebraic Methodology and Software Technology, AMAST 2004, held in Stirling, Scotland, UK in July 2004. The 35 revised full papers presented together with abstracts of 5 invited talks and an invited paper were carefully reviewed and selected from 63 submissions. Among the topics covered are all current issues in formal methods related to algebraic approaches to software engineering including abstract data types, process algebras, algebraic specification, model checking, abstraction, refinement, model checking, state machines, rewriting, Kleene algebra, programming logic, etc. Front Matter....Pages - Algebraic Approaches to Problem Generalisation....Pages 1-2 A Science of Software Design....Pages 3-18 Glass Box and Black Box Views of State-Based System Specifications....Pages 19-19 Abstraction for Safety, Induction for Liveness....Pages 20-20 Counting Votes with Formal Methods....Pages 21-22 Agent-Oriented Programming: Where Do We Stand?....Pages 23-26 On Guard: Producing Run-Time Checks from Integrity Constraints....Pages 27-41 Behavioural Types and Component Adaptation....Pages 42-56 Towards Correspondence Carrying Specifications....Pages 57-71 Formalizing and Proving Semantic Relations between Specifications by Reflection....Pages 72-86 Model-Checking Systems with Unbounded Variables without Abstraction....Pages 87-101 A Generic Software Safety Document Generator....Pages 102-116 Linear Temporal Logic and Z Refinement....Pages 117-131 Formal JVM Code Analysis in JavaFAN....Pages 132-147 Verifying a Sliding Window Protocol in μ CRL....Pages 148-163 State Space Reduction for Process Algebra Specifications....Pages 164-180 A Hybrid Logic of Knowledge Supporting Topological Reasoning....Pages 181-195 A Language for Configuring Multi-level Specifications....Pages 196-210 Flexible Proof Reuse for Software Verification....Pages 211-225 Deductive Verification of Distributed Groupware Systems....Pages 226-240 Formal Verification of a Commercial Smart Card Applet with Multiple Tools....Pages 241-257 Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs....Pages 258-273 Refining Mobile UML State Machines....Pages 274-288 Verifying Invariants of Component-Based Systems through Refinement....Pages 289-303 Modelling Concurrent Interactions....Pages 304-318 Proof Support for RAISE by a Reuse Approach Based on Institutions....Pages 319-333 Separate Compositional Analysis of Class-Based Object-Oriented Languages....Pages 334-348 Abstract Domains for Property Checking Driven Analysis of Temporal Properties....Pages 349-363 Modular Rewriting Semantics of Programming Languages....Pages 364-378 Modal Kleene Algebra and Partial Correctness....Pages 379-393 Modularity and the Rule of Adaptation....Pages 394-408 Modal Abstractions in μ CRL....Pages 409-425 Semantics of Plan Revision in Intelligent Agents....Pages 426-442 Generic Exception Handling and the Java Monad....Pages 443-459 Expressing Iterative Properties Logically in a Symbolic Setting....Pages 460-474 Extending Separation Logic with Fixpoints and Postponed Substitution....Pages 475-490 A Formally Verified Calculus for Full Java Card....Pages 491-505 On Refinement of Generic State-Based Software Components....Pages 506-520 Techniques for Executing and Reasoning about Specification Diagrams....Pages 521-536 Formalising Graphical Behaviour Descriptions....Pages 537-552 Model-Checking Distributed Real-Time Systems with States, Events, and Multiple Fairness Assumptions....Pages 553-567 Back Matter....Pages - Algebraic Methodology and Software Technology: 10th International Conference, AMAST 2004, Stirling, Scotland, UK, July 12-16, 2004. Proceedings Author: Charles Rattray, Savitri Maharaj, Carron Shankland Published by Springer Berlin Heidelberg ISBN: 978-3-540-22381-8 DOI: 10.1007/b98770 Table of Contents: Algebraic Approaches to Problem Generalisation A Science of Software Design Glass Box and Black Box Views of State-Based System Specifications Abstraction for Safety, Induction for Liveness Counting Votes with Formal Methods Agent-Oriented Programming: Where Do We Stand? On Guard: Producing Run-Time Checks from Integrity Constraints Behavioural Types and Component Adaptation Towards Correspondence Carrying Specifications Formalizing and Proving Semantic Relations between Specifications by Reflection Model-Checking Systems with Unbounded Variables without Abstraction A Generic Software Safety Document Generator Linear Temporal Logic and Z Refinement Formal JVM Code Analysis in JavaFAN Verifying a Sliding Window Protocol in μCRL State Space Reduction for Process Algebra Specifications A Hybrid Logic of Knowledge Supporting Topological Reasoning A Language for Configuring Multi-level Specifications Flexible Proof Reuse for Software Verification Deductive Verification of Distributed Groupware Systems A common technique for solving programming problems is to express the problem in terms of solving a system of so-called "simultaneous" equations (a collection of equations in a number of unknowns that are often mutually recursive).