Verification and code generation for invariant diagrams in Isabelle

DOI10.1016/J.JLAP.2013.09.001zbMATH Open1304.68032OpenAlexW2029872263MaRDI QIDQ478381FDOQ478381

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

Recommendations

• Invariant based programming: Basic approach and teaching experiences
• Invariant diagrams with data refinement
• A verified compiler from Isabelle/HOL to CakeML
• Publication:2754111
• Imperative Functional Programming with Isabelle/HOL

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)

Cites Work

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

Cited In (3)

• Title not available (Why is that?)
• Stream Fusion for Isabelle’s Code Generator
• Invariant diagrams with data refinement

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)