An integrated approach to high integrity software verification

DOI10.1007/s10817-006-9034-1zbMath1107.68032OpenAlexW2113487529WikidataQ122898377 ScholiaQ122898377MaRDI QIDQ861714

Andrew Ireland, Roderick Chapman, Janet Barnes, Bill J. Ellis, Andrew W. Cook

Publication date: 30 January 2007

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-006-9034-1

zbMATH Keywords

automated reasoningSPARK Approach

Mathematics Subject Classification ID

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

Uses Software

• Stratego
• Ada95
• SPARK
• SLAM
• PURRS
• ESC/Java
• NQTHM
• Houdini
• CLAM
• ICS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Rippling: A heuristic for guiding inductive proofs
• Experiments with proof plans for induction
• Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
• Proof planning for strategy development
• A general setting for flexibly combining and augmenting decision procedures
• Productive use of failure in inductive proof
• Middle-out reasoning for synthesis and induction
• A calculus for and termination of rippling
• Grammar Analysis and Parsing by Abstract Interpretation
• Logical analysis of programs
• Automatic verification of functions with accumulating parameters
• AutoBayes: a system for generating data analysis programs from statistical models
• Information-flow and data-flow analysis of while-programs
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• An axiomatic basis for computer programming
• Programming Languages and Systems

This page was built for publication: An integrated approach to high integrity software verification