Static Contract Checking with Abstract Interpretation

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

Mathematics Subject Classification ID

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

• Apron
• KRAKATOA
• Why3
• Caduceus
• ESC/Java
• Pex
• VeriFast
• Boogie
• JACK
• VeriCool
• jStar
• Octagon
• ASTREE
• FunArray

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