Algebraic Methodology and Software Technology
13th International Conference, AMAST 2010, Lac-Beauport, QC, Canada, June 23-25, 2010, Revised Selected Papers
Published on 14. January 2011
X, 238 pages
978-3-642-17796-5 (ISBN)
Description
This book constitutes the refereed proceedings of the 13th International Conference on Algebraic Methodology and Software Technology, AMAST 2010, held in Lac-Beauport, QC, Canada, in June 2010.
The 14 revised full papers presented were carefully reviewed and selected from 33 submissions. The papers are organized in 1 invited paper, 10 contributed research papers, and 4 system demonstrations.
More details
Other editions
Additional editions
Michael Johnson | Dusko Pavlovic
Algebraic Methodology and Software Technology
13th International Conference, AMAST 2010, Lac-Beauport, QC, Canada, June 23-25, 2010, Revised Selected Papers
Book
01/2011
Springer
€53.49
Shipment within 5-7 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Part 1. Invited Paper
- Structural Analysis for Stochastic Process Algebra Models
- Introduction
- The PEPA Modelling Formalism
- Introduction to PEPA
- Numerical Representation of PEPA Models
- Place/Transtion Structure Underlying PEPA Models
- P/T Systems
- Example
- Invariance in PEPA Models
- Example
- Liveness in PEPA Models
- Linearisation of State Space for PEPA
- Linearisation of State Space
- Example
- Improved Deadlock-Checking Methods for PEPA
- Equivalent Deadlock-Checking
- Deadlock-Checking Algorithm in LRSPsf
- Examples
- Related Work
- Conclusions
- References
- Part 2. Contributed Research Papers
- Verification of Common Interprocedural Compiler Optimizations Using Visibly Pushdown Kleene Algebra
- Introduction
- Visibly Pushdown Regular Expressions (VPRE)
- Visibly Pushdown Kleene Algebra (VPKA)
- Visibly Pushdown Kleene Algebra with Tests
- Metablocks
- Verification of Common Interprocedural Compiler Optimizations
- Interprocedural Dead Code Elimination
- Inlining of Functions
- Tail-Recursion Elimination
- Procedure Reordering
- Function Cloning
- Discussion
- Conclusion
- References
- On the Expressiveness of the p-Calculus and the Mobile Ambients
- Introduction
- The Mobile Ambients
- The -Calculus
- The Encoding
- Conclusion and Future Work
- References
- Integrating Maude into Hets
- Introduction
- Hets
- Rewriting Logic and Maude
- Relating the Maude and CASL Logics
- Maude
- CASL
- Encoding Maude in CASL
- From Maude Modules to Development Graphs
- Normalization of Free Definition Links
- An Example: Reversing Lists
- Conclusions and Future Work
- References
- Model Refinement Using Bisimulation Quotients
- Introduction
- Model Classes and Bisimulation Classes
- Prerequisites and Notational Conventions
- Model Classes
- Bisimulation Classes
- Algorithms Generating Bisimulation Equivalences
- Generic Refinement Using Finite Abstract Models
- Construction of an Adequate Expansion Operation
- Preservation of Satisfactory Refinements under Expansion
- A Generic Algorithm for Model Refinement by Abstraction
- A Summary of Typical Applications
- Related Work and Conclusion
- References
- Type Fusion
- Introduction
- Background
- Initial Algebras and Final Coalgebras
- Adjoint Folds and Unfolds
- Type Fusion
- Application: Firstification
- Application: Type Specialisation
- Application: Tabulation
- Related Work
- References
- Coalgebraic Semantics for Parallel Derivation Strategies in Logic Programming
- Introduction
- Logic Programs and SLD Derivations
- Finite and Infinite Computations by Logic Programs
- Coalgebraic Semantics for Ground Logic Programs
- Coalgebraic Semantics and Parallel Execution of Logic Programs
- Conclusions
- References
- Learning in a Changing World, an Algebraic Modal Logical Approach
- Introduction
- The Algebra of Di-systems
- Navigation Di-systems
- Applications to Navigation
- Map-Based Navigation
- Staircase Navigation
- Grid Navigation
- Embedding Epistemic Systems
- Conclusions and Future Work
- References
- Matching Logic: An Alternative to Hoare/Floyd Logic
- Introduction
- Preliminaries, the IMP Language, and Hoare Logic
- Matching Logic
- Equivalence of Hoare and (A Restricted Form of) Matching Logic
- H2M: From Hoare to Matching Logic
- M2H: From Matching to Hoare Logic
- Adding a Heap
- Proof Example and Practical Experience
- Conclusion, Related Work and Future Work
- References
- Program Calculation in Coq
- Introduction
- Coq Tactics for Program Calculation
- Overview of Available Tactics
- More Advanced Use
- Behind the Scene
- Application: BMF in Coq
- Examples
- Implementation of Partial Functions
- Exploiting Different Views of a Data Type
- Imposing Constraints on a Higher-Order Function
- Related Work
- Conclusion and Future Work
- References
- Cooperation of Algebraic Constraint Domains in Higher-Order Functional and Logic Programming
- Introduction
- Higher-Order Algebraic Constraint Cooperation
- A Higher-Order Constraint Domain
- Preliminary Notions
- The Higher-Order Constraint Domain
- The -Constraint Solver
- Higher-Order Coordination of Algebraic Domains
- Higher-Order Cooperative Programming in CFLP(C)
- Conclusions
- References
- Part 3. System Demonstrations
- Proving Termination Properties with mu-term
- Introduction
- Structure and Functionality of mu-term 5.0
- Proving Termination of Context-Sensitive Rewriting
- Proving Termination of Innermost CSR
- Proving Termination of Order-Sorted Rewriting
- Proving Termination of AC-Rewriting
- Use of Rational Polynomials and Matrix Interpretations
- Termination Expert
- External Use of mu-term
- Conclusions
- References
- BAL Tool in Flexible Manufacturing Systems
- Motivation
- BAL Tool
- Graphical Interface and Assistant
- Industrial Case Study - Flexible Manufacturing System
- Conclusions and Future Work
- References
- A Complete Declarative Debugger for Maude
- Introduction
- Using the Debugger
- Debugging Sessions
- Conclusions
- References
- An Assume Guarantee Approach for Checking Quantified Array Assertions
- Introduction
- Examples
- Pre-recursive Case (insertion_sort)
- Post-Recursive Case (selection_sort)
- Experimental Results
- Conclusion
- References
- Author Index
