Completeness of ASM Refinement

DOI10.1016/j.entcs.2008.06.003zbMath1283.68213OpenAlexW2095211351MaRDI QIDQ5403462

Gerhard Schellhorn

Publication date: 26 March 2014

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.06.003

zbMATH Keywords

completenessrefinementabstract state machinesIO automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (4)

A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures ⋮ Starvation-free mutual exclusion with semaphores ⋮ Simulation refinement for concurrency verification ⋮ Flashix: modular verification of a concurrent and crash-safe flash file system

Uses Software

• KIV
• Z

Cites Work

• ASM refinement and generalizations of forward simulation in data refinement: a comparison
• The ASM refinement method
• The existence of refinement mappings
• Proving correctness with respect to nondeterministic safety specifications
• Power domains
• Relation-algebraic semantics
• Forward and backward simulations. I. Untimed Systems
• Universal extensions to simulate specifications
• Splitting forward simulations to cope with liveness
• Programs, Recursion and Unbounded Choice
• Abstract State Machines
• Data Refinement
• Evolving Algebras 1993: Lipari Guide
• Eternity variables to prove simulation of specifications
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Completeness of ASM Refinement