Modular inference of subprogram contracts for safety checking
type: Item
instance of: scholarly article
title: Modular inference of subprogram contracts for safety checking
zbMATH Open document ID: 1213.68385
author: Yannick Moy
author: Claude Marché
published in: Journal of Symbolic Computation
publication date: 2010-11-10T00:00:00Z
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 5814771
zbMATH Keywords: specification languages
zbMATH Keywords: functional behavior
zbMATH Keywords: contracts
zbMATH Keywords: inference
zbMATH Keywords: abstract interpretation
zbMATH Keywords: weakest precondition
zbMATH Keywords: quantifier elimination
describes a project that uses: Spec#
describes a project that uses: Houdini
describes a project that uses: KRAKATOA
describes a project that uses: ACSL
describes a project that uses: JML
describes a project that uses: Caduceus
describes a project that uses: Alt-Ergo
describes a project that uses: Octagon
describes a project that uses: Why3
describes a project that uses: VCC
describes a project that uses: Cyclone
MaRDI profile type: Publication
full work available at URL: j.jsc.2010.06.004
OpenAlex ID: W2013252208
cites work: Q5310200
cites work: Computer Aided Verification
cites work: ``A la Burstall'' intermittent assertions induction principles for proving inevitability properties of programs
cites work: Q4144755
cites work: Verification of non-functional programs using interpretations in type theory
cites work: Q2763999
cites work: Assertion Checking Unified
cites work: Behavioral interface specification languages
cites work: Affine relationships among variables of a program
cites work: Programming Languages and Systems
cites work: Q4779116
cites work: The octagon abstract domain
cites work: A Quantifier Elimination Algorithm for Linear Real Arithmetic
cites work: Static Analysis
cites work: Polymorphic type, region and effect inference
cites work: Region-based memory management
cites work: Q4226937
DOI: 10.1016/J.JSC.2010.06.004
Recommended article: Modular Safety Checking for Fine-Grained Concurrency
Recommended article: Context-Sensitive Multivariant Assertion Checking in Modular Programs
Recommended article: Modular Verification of Recursive Programs
Recommended article: A foundation for modular reasoning about safety and progress properties of state-based concurrent programs
Recommended article: Abstraction and subsumption in modular verification of C programs
Recommended article: Model Checking Safety Properties in Modular High-Level Nets
Recommended article: Modular verification of programs with effects and effects handlers
Recommended article: Modular Verification of Higher-Order Functional Programs
Recommended article: Q4036556
description: scientific article; zbMATH DE number 5814771