Verification and code generation for invariant diagrams in Isabelle
type: Item
instance of: scholarly article
title: Verification and code generation for invariant diagrams in Isabelle
zbMATH Open document ID: 1304.68032
author: Viorel Preoteasa
author: Ralph-Johan Back
author: Johannes Eriksson
published in: Journal of Logical and Algebraic Methods in Programming
publication date: 2014-12-03T00:00:00Z
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 6376568
zbMATH Keywords: invariant-based programming
zbMATH Keywords: invariant diagrams
zbMATH Keywords: verification conditions
zbMATH Keywords: Isabelle proof assistant
zbMATH Keywords: correctness
zbMATH Keywords: recursive functions
zbMATH Keywords: proof automation
describes a project that uses: HOL-Boogie
describes a project that uses: Isabelle
describes a project that uses: Isabelle/HOL
describes a project that uses: Sledgehammer
describes a project that uses: Locales
MaRDI profile type: Publication
full work available at URL: j.jlap.2013.09.001
OpenAlex ID: W2029872263
cites work: Invariant based programming: Basic approach and teaching experiences
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Sledgehammer: Judgement Day
cites work: Code Generation via Higher-Order Rewrite Systems
cites work: HOL-Boogie -- an interactive prover-backend for the verifying C compiler
cites work: Q4809043
cites work: Proof-producing synthesis of ML from higher-order logic
cites work: The size-change principle for program termination
cites work: Types for Proofs and Programs
DOI: 10.1016/J.JLAP.2013.09.001
description: scientific article; zbMATH DE number 6376568