Completeness of ASM refinement

DOI10.1016/J.ENTCS.2008.06.003MaRDI QIDQ5403462zbMATH OpenOpenAlexFDO

Authors 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

abstract state machinescompletenessIO automatarefinement

Mathematics Subject Classification ID

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

Recommendations

• Completeness of fair ASM refinement
• ASM refinement and generalizations of forward simulation in data refinement: a comparison
• The ASM refinement method
• ASM refinement preserving invariants
• scientific article; zbMATH DE number 1617299

Cites work

• Abstract State Machines
• ASM refinement and generalizations of forward simulation in data refinement: a comparison
• ASM refinement preserving invariants
• Data Refinement
• Eternity variables to prove simulation of specifications
• Evolving Algebras 1993: Lipari Guide
• Forward and backward simulations. I. Untimed Systems
• scientific article; zbMATH DE number 1615985 (Why is no real title available?)
• scientific article; zbMATH DE number 3707731 (Why is no real title available?)
• scientific article; zbMATH DE number 18622 (Why is no real title available?)
• scientific article; zbMATH DE number 42431 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1354178 (Why is no real title available?)
• scientific article; zbMATH DE number 605917 (Why is no real title available?)
• scientific article; zbMATH DE number 1948157 (Why is no real title available?)
• scientific article; zbMATH DE number 2013580 (Why is no real title available?)
• scientific article; zbMATH DE number 1487738 (Why is no real title available?)
• scientific article; zbMATH DE number 1543041 (Why is no real title available?)
• scientific article; zbMATH DE number 1552508 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 2090023 (Why is no real title available?)
• scientific article; zbMATH DE number 773979 (Why is no real title available?)
• Power domains
• Programs, Recursion and Unbounded Choice
• Proving correctness with respect to nondeterministic safety specifications
• Relation-algebraic semantics
• Splitting forward simulations to cope with liveness
• The ASM refinement method
• The existence of refinement mappings
• The WAM case study: Verifying compiler correctness for Prolog with KIV
• Universal extensions to simulate specifications

Cited in

(7)

• Flashix: modular verification of a concurrent and crash-safe flash file system
• A sound and complete proof technique for linearizability of concurrent data structures
• ASM refinement preserving invariants
• Starvation-free mutual exclusion with semaphores
• Simulation refinement for concurrency verification
• Completeness of fair ASM refinement
• ASM refinement and generalizations of forward simulation in data refinement: a comparison

Describes a project that uses

Uses Software

• KIV
• Z

This page was built for publication: Completeness of ASM refinement

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5403462)