Static contract checking with abstract interpretation

DOI10.1007/978-3-642-18070-5_2MaRDI QIDQ3067530zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Precondition inference from intermittent assertions and application to contracts on collections
• Modular inference of subprogram contracts for safety checking
• scientific article; zbMATH DE number 1953022
• Static contract checking for Haskell
• scientific article; zbMATH DE number 2104620

Cites work

• scientific article; zbMATH DE number 1948392 (Why is no real title available?)
• scientific article; zbMATH DE number 1953274 (Why is no real title available?)
• A framework for numeric analysis of array operations
• A parametric segmentation functor for fully automatic and scalable array content analysis
• Abstract interpretation and application to logic programs
• Affine relationships among variables of a program
• Applications of polyhedral computations to the analysis and verification of hardware and software systems
• Array Abstractions from Proofs
• Generating all vertices of a polyhedron is hard
• Lifting abstract interpreters to quantified logical domains
• Pentagons: a weakly relational abstract domain for the efficient validation of array accesses
• Precondition inference from intermittent assertions and application to contracts on collections
• Program Analysis Using Symbolic Ranges
• Programming Languages and Systems
• Static Analysis
• SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities
• Systematic design of program transformation frameworks by abstract interpretation
• The octagon abstract domain
• Two variables per linear inequality as an abstract domain
• Verification, Model Checking, and Abstract Interpretation

Cited in

(15)

• A generic framework for heap and value analyses of object-oriented programming languages
• Contract-based verification of MATLAB-style matrix programs
• Unbounded procedure summaries from bounded environments
• An extension of lazy abstraction with interpolation for programs with arrays
• Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption
• Incremental and modular context-sensitive analysis
• Bit-vector typestate analysis
• scientific article; zbMATH DE number 1953020 (Why is no real title available?)
• Demand-driven interprocedural analysis for map-based abstract domains
• Soft contract verification
• Practical run-time checking via unobtrusive property caching
• Precondition inference from intermittent assertions and application to contracts on collections
• Automatic inference of access permissions
• Higher order symbolic execution for contract verification and refutation
• Checking compatibility of bit sizes in floating point comparison operations

Describes a project that uses

Uses Software

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

This page was built for publication: Static contract checking with abstract interpretation

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