Modular inference of subprogram contracts for safety checking

DOI10.1016/J.JSC.2010.06.004MaRDI QIDQ604392zbMATHOpenAlexFDO

Authors Yannick Moy, Claude Marché

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

inferenceabstract interpretationcontractsspecification languagesquantifier eliminationweakest preconditionfunctional behavior

Mathematics Subject Classification ID

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

Recommendations

• Modular Safety Checking for Fine-Grained Concurrency
• Context-Sensitive Multivariant Assertion Checking in Modular Programs
• Modular Verification of Recursive Programs
• A foundation for modular reasoning about safety and progress properties of state-based concurrent programs
• Abstraction and subsumption in modular verification of C programs
• Model checking safety properties in modular high-level nets
• Modular verification of programs with effects and effects handlers
• Modular verification of higher-order functional programs
• scientific article; zbMATH DE number 176727

Cites work

• scientific article; zbMATH DE number 1693447 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1253963 (Why is no real title available?)
• scientific article; zbMATH DE number 1834573 (Why is no real title available?)
• scientific article; zbMATH DE number 5194318 (Why is no real title available?)
• A Quantifier Elimination Algorithm for Linear Real Arithmetic
• Affine relationships among variables of a program
• Assertion Checking Unified
• Behavioral interface specification languages
• Computer Aided Verification
• Polymorphic type, region and effect inference
• Programming Languages and Systems
• Region-based memory management
• Static Analysis
• The octagon abstract domain
• Verification of non-functional programs using interpretations in type theory
• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs

Cited in

(13)

• Static contract checking with abstract interpretation
• An active learning approach to synthesizing program contracts
• Modular set-based analysis from contracts
• Automatically proving termination and memory safety for programs with pointer arithmetic
• ExplainHoudini: making Houdini inference transparent
• Hoare-style reasoning from multiple contracts
• Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework
• Annotation inference for modular checkers
• Sufficient Preconditions for Modular Assertion Checking
• Precondition inference from intermittent assertions and application to contracts on collections
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• Automated inference of library specifications for source-sink property verification
• Symbolic abstract contract synthesis in a rewriting framework

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q604392)