Algebraic Methodology and Software Technology

Name: Algebraic Methodology and Software Technology | 13th International Conference, AMAST 2010, Lac-Beauport, QC, Canada, June 23-25, 2010, Revised Selected Papers
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

13th International Conference, AMAST 2010, Lac-Beauport, QC, Canada, June 23-25, 2010, Revised Selected Papers

Michael Johnson Dusko Pavlovic(Herausgeber*in)

Springer (Verlag)

Erschienen am 14. Januar 2011

X, 238 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-17796-5 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken