Modular inference of subprogram contracts for safety checking

DOI10.1016/j.jsc.2010.06.004zbMath1213.68385OpenAlexW2013252208MaRDI QIDQ604392

Claude Marché, Yannick Moy

Publication date: 10 November 2010

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jsc.2010.06.004

zbMATH Keywords

quantifier eliminationspecification languagesinferencecontractsabstract interpretationweakest preconditionfunctional behavior

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (3)

Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Formal verification of numerical programs: from C annotated programs to mechanical proofs ⋮ Abstract Contract Synthesis and Verification in the Symbolic 𝕂 Framework

Uses Software

• KRAKATOA
• ACSL
• Why3
• JML
• Spec#
• Caduceus
• Alt-Ergo
• VCC
• Cyclone
• Octagon
• Houdini

Cites Work

• Region-based memory management
• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
• The octagon abstract domain
• Affine relationships among variables of a program
• Behavioral interface specification languages
• Verification of non-functional programs using interpretations in type theory
• Polymorphic type, region and effect inference
• Assertion Checking Unified
• Programming Languages and Systems
• A Quantifier Elimination Algorithm for Linear Real Arithmetic
• Static Analysis
• Computer Aided Verification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Modular inference of subprogram contracts for safety checking