On using data abstractions for model checking refinements

DOI10.1007/s00236-007-0042-3zbMath1111.68077OpenAlexW1966707489MaRDI QIDQ878378

John Derrick, Heike Wehrheim

Publication date: 26 April 2007

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00236-007-0042-3

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (1)

Checking Z Data Refinements Using Traces Refinement

Uses Software

• Z/EVES
• Z
• FDR2

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Relational concurrent refinement
• Verifying data refinements using a model checker
• Process simulation and refinement
• A state-based approach to communicating processes
• Property preserving abstractions for the verification of concurrent systems
• A hierarchy of failures-based models: theory and application
• A singleton failures semantics for communicating sequential processes
• Counterexample-guided abstraction refinement for symbolic model checking
• Grammar Analysis and Parsing by Abstract Interpretation
• Data Refinement
• Abstract Interpretation Frameworks
• ZB 2005: Formal Specification and Development in Z and B
• Integrated Formal Methods
• Data abstraction techniques in the validation of CSP-OZ specifications
• Model-checking CSP-Z: Strategy, tool support and industrial application
• Specification, refinement and verification of concurrent systems -- an integration of Object-\(Z\) and \(CSP\)

This page was built for publication: On using data abstractions for model checking refinements