An integrated approach to high integrity software verification
type: Item
instance of: scholarly article
title: An integrated approach to high integrity software verification
zbMATH Open document ID: 1107.68032
author: Andrew Ireland
author: Bill J. Ellis
author: Roderick Chapman
author: Janet Barnes
author: Andrew W. Cook
published in: Journal of Automated Reasoning
publication date: 2007-01-30T00:00:00Z
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 5119743
zbMATH Keywords: automated reasoning
zbMATH Keywords: SPARK Approach
Wikidata QID: Q122898377
describes a project that uses: SPARK
describes a project that uses: CLAM
describes a project that uses: NQTHM
describes a project that uses: Houdini
describes a project that uses: SLAM
describes a project that uses: Stratego
describes a project that uses: PURRS
describes a project that uses: ESC/Java
describes a project that uses: ICS
describes a project that uses: Ada95
MaRDI profile type: Publication
full work available at URL: s10817-006-9034-1
OpenAlex ID: W2113487529
cites work: A calculus for and termination of rippling
cites work: Information-flow and data-flow analysis of while-programs
cites work: AutoBayes: a system for generating data analysis programs from statistical models
cites work: Q4040283
cites work: Rippling: Meta-Level Guidance for Mathematical Reasoning
cites work: Rippling: A heuristic for guiding inductive proofs
cites work: Experiments with proof plans for induction
cites work: Grammar Analysis and Parsing by Abstract Interpretation
cites work: Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
cites work: Q5683688
cites work: Q4553256
cites work: Q2763999
cites work: Q5584402
cites work: An axiomatic basis for computer programming
cites work: Productive use of failure in inductive proof
cites work: Automatic verification of functions with accumulating parameters
cites work: Proof planning for strategy development
cites work: A general setting for flexibly combining and augmenting decision procedures
cites work: Logical analysis of programs
cites work: Middle-out reasoning for synthesis and induction
cites work: Q4255591
cites work: Programming Languages and Systems
cites work: Q2778890
DOI: 10.1007/S10817-006-9034-1
description: scientific article; zbMATH DE number 5119743