Static Contract Checking with Abstract Interpretation
From MaRDI portal
Publication:3067530
DOI10.1007/978-3-642-18070-5_2zbMath1308.68033OpenAlexW1657354101MaRDI QIDQ3067530
Manuel Fähndrich, Francesco Logozzo
Publication date: 21 January 2011
Published in: Formal Verification of Object-Oriented Software (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-18070-5_2
Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
A generic framework for heap and value analyses of object-oriented programming languages ⋮ Contract-based verification of MATLAB-style matrix programs ⋮ Automatic Inference of Access Permissions ⋮ Practical run-time checking via unobtrusive property caching ⋮ Higher order symbolic execution for contract verification and refutation ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ Unbounded procedure summaries from bounded environments ⋮ Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption ⋮ Checking Compatibility of Bit Sizes in Floating Point Comparison Operations ⋮ Demand-driven interprocedural analysis for map-based abstract domains ⋮ Incremental and Modular Context-sensitive Analysis ⋮ Precondition Inference from Intermittent Assertions and Application to Contracts on Collections
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- The octagon abstract domain
- Pentagons: a weakly relational abstract domain for the efficient validation of array accesses
- Applications of polyhedral computations to the analysis and verification of hardware and software systems
- Affine relationships among variables of a program
- Precondition Inference from Intermittent Assertions and Application to Contracts on Collections
- Two Variables per Linear Inequality as an Abstract Domain
- Lifting abstract interpreters to quantified logical domains
- SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities
- Program Analysis Using Symbolic Ranges
- Abstract interpretation and application to logic programs
- Systematic design of program transformation frameworks by abstract interpretation
- A framework for numeric analysis of array operations
- Programming Languages and Systems
- A parametric segmentation functor for fully automatic and scalable array content analysis
- Array Abstractions from Proofs
- Static Analysis
- Verification, Model Checking, and Abstract Interpretation
- Generating all vertices of a polyhedron is hard