Modular inference of subprogram contracts for safety checking
From MaRDI portal
(Redirected from Publication:604392)
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)- Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework
- Annotation inference for modular checkers
- Symbolic abstract contract synthesis in a rewriting framework
- Modular set-based analysis from contracts
- Hoare-style reasoning from multiple contracts
- Static contract checking with abstract interpretation
- Sufficient Preconditions for Modular Assertion Checking
- 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
- Automated inference of library specifications for source-sink property verification
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- An active learning approach to synthesizing program contracts
Describes a project that uses
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)
