Verification and code generation for invariant diagrams in Isabelle

DOI10.1016/j.jlap.2013.09.001zbMath1304.68032OpenAlexW2029872263MaRDI QIDQ478381

Ralph-Johan Back, Viorel Preoteasa, 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

correctnessrecursive functionsproof automationverification conditionsinvariant diagramsinvariant-based programmingIsabelle proof assistant

Mathematics Subject Classification ID

Uses Software

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

Cites Work

• Unnamed Item
• Invariant based programming: Basic approach and teaching experiences
• Isabelle/HOL. A proof assistant for higher-order logic
• HOL-Boogie -- an interactive prover-backend for the verifying C compiler
• Code Generation via Higher-Order Rewrite Systems
• Proof-producing synthesis of ML from higher-order logic
• The size-change principle for program termination
• Types for Proofs and Programs
• Sledgehammer: Judgement Day

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