Model checking Z specifications using SAL

DOI10.1007/11415787_6MaRDI QIDQ5703821zbMATH OpenOpenAlexFDO

Authors Graeme Smith, Luke Wildman

Publication date 10 November 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b135596

zbMATH Keywords

model checkingSALtool supportZ

Mathematics Subject Classification ID

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

Recommendations

• Z2SAL: a translation-based model checker for Z
• Model checking Object-Z using ASM
• A ZDD-Based Efficient Higher-Order Model Checking Algorithm
• Constructive consistency checking for partial specification in Z
• Model-checking CSP-Z: Strategy, tool support and industrial application
• Zing: A model checker for concurrent software
• SAT-Based Model Checking

Cited in

(13)

• Temporal-logic property preservation under Z refinement
• Constructive consistency checking for partial specification in Z
• Symbolic analysis of transition systems
• A Z approach in validating ORA-SS data models
• Property transformation under specification change
• Mechanization of an integrated approach: Shallow embedding into SAL/PVS
• Model checking RAISE applicative specifications
• SAL 2
• Z2SAL: a translation-based model checker for Z
• Alloy as a refactoring checker?
• Compensation by design
• Verifying data refinements using a model checker
• On using data abstractions for model checking refinements

Describes a project that uses

Uses Software

• Z/EVES

This page was built for publication: Model checking Z specifications using SAL

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