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.
Author(s): Roland Backhouse (auth.), Charles Rattray, Savitri Maharaj, Carron Shankland (eds.)
Series: Lecture Notes in Computer Science 3116
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2004
Language: English
Pages: 572
Tags: Logics and Meanings of Programs; Mathematical Logic and Formal Languages; Software Engineering; Programming Techniques; Symbolic and Algebraic Manipulation; Artificial Intelligence (incl. Robotics)
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 -
