Invariant diagrams with data refinement

DOI10.1007/S00165-011-0195-2zbMath1242.68074OpenAlexW2006030419MaRDI QIDQ432148

Ralph-Johan Back, Viorel Preoteasa

Publication date: 3 July 2012

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-011-0195-2

zbMATH Keywords

data refinementgraph markinginvariant based programmingmechanical verification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• Isabelle/HOL
• Archive Formal Proofs
• Data Refinement IBP
• Deutsch Schorr Waite

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• Proving pointer programs in higher-order logic
• Proof of correctness of data representations
• Data Refinement of Invariant Based Programs
• Programming with Verification Conditions
• Refinement Calculus
• An efficient machine-independent procedure for garbage collection in various list structures
• Encoding, decoding and data refinement

This page was built for publication: Invariant diagrams with data refinement