Data refinement of invariant based programs

DOI10.1016/J.ENTCS.2009.12.022MaRDI QIDQ2994494zbMATH OpenOpenAlexFDO

Authors Viorel Preoteasa, Ralph-Johan Back

Publication date 1 August 2016

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.2009.12.022

zbMATH Keywords

data refinementinvariant-based programmingmechanical verification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Invariant diagrams with data refinement
• Data refinement of predicate transformers
• Data refinement by calculation
• Stepwise refinement of heap-manipulating code in Chalice
• Some proofs of data refinement

Cites work

• An efficient machine-independent procedure for garbage collection in various list structures
• Encoding, decoding and data refinement
• scientific article; zbMATH DE number 3705887 (Why is no real title available?)
• scientific article; zbMATH DE number 1178976 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Proof of correctness of data representations
• Proving pointer programs in higher-order logic
• Refinement Calculus

Cited in

(9)

• Algebra of monotonic Boolean transformers
• Data Refinement IBP
• Deutsch Schorr Waite
• Pseudo Hoops
• Invariant diagrams with data refinement
• scientific article; zbMATH DE number 2079998 (Why is no real title available?)
• Formalization of Refinement Calculus for Reactive Systems
• Lattice Properties
• Algebra of Monotonic Boolean Transformers

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Data refinement of invariant based programs

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