Modular inference of subprogram contracts for safety checking
From MaRDI portal
Publication:604392
DOI10.1016/J.JSC.2010.06.004zbMATH Open1213.68385OpenAlexW2013252208MaRDI QIDQ604392FDOQ604392
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
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
inferenceabstract interpretationcontractsspecification languagesquantifier eliminationweakest preconditionfunctional behavior
Cites Work
- The octagon abstract domain
- Title not available (Why is that?)
- Title not available (Why is that?)
- Affine relationships among variables of a program
- ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
- Title not available (Why is that?)
- Polymorphic type, region and effect inference
- Computer Aided Verification
- Verification of non-functional programs using interpretations in type theory
- A Quantifier Elimination Algorithm for Linear Real Arithmetic
- Behavioral interface specification languages
- Region-based memory management
- Programming Languages and Systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- Assertion Checking Unified
- Static Analysis
Cited In (8)
- Annotation inference for modular checkers
- Static contract checking with abstract interpretation
- Sufficient Preconditions for Modular Assertion Checking
- Abstract Contract Synthesis and Verification in the Symbolic 𝕂 Framework
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Precondition inference from intermittent assertions and application to contracts on collections
- ExplainHoudini: making Houdini inference transparent
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
Uses Software
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)
