Verification and code generation for invariant diagrams in Isabelle

DOI10.1016/J.JLAP.2013.09.001MaRDI QIDQ478381zbMATH OpenOpenAlexFDO

Authors Viorel Preoteasa, Ralph-Johan Back, Johannes Eriksson

Publication date 3 December 2014

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlap.2013.09.001

zbMATH Keywords

proof automationrecursive functionscorrectnessverification conditionsinvariant diagramsinvariant-based programmingIsabelle proof assistant

Mathematics Subject Classification ID

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

Recommendations

• Invariant based programming: Basic approach and teaching experiences
• Invariant diagrams with data refinement
• A verified compiler from Isabelle/HOL to CakeML
• scientific article; zbMATH DE number 1670798
• Imperative Functional Programming with Isabelle/HOL

Cites work

• scientific article; zbMATH DE number 2090288 (Why is no real title available?)
• Code generation via higher-order rewrite systems
• HOL-Boogie -- an interactive prover-backend for the verifying C compiler
• Invariant based programming: Basic approach and teaching experiences
• Isabelle/HOL. A proof assistant for higher-order logic
• Proof-producing synthesis of ML from higher-order logic
• Sledgehammer: judgement day
• The size-change principle for program termination
• Types for Proofs and Programs

Cited in

(3)

• Invariant diagrams with data refinement
• scientific article; zbMATH DE number 1670798 (Why is no real title available?)
• Stream Fusion for Isabelle’s Code Generator

Describes a project that uses

Uses Software

• HOL-Boogie
• Isabelle
• Isabelle/HOL
• Sledgehammer
• Locales

This page was built for publication: Verification and code generation for invariant diagrams in Isabelle

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