A parametric segmentation functor for fully automatic and scalable array content analysis

DOI10.1145/1926385.1926399MaRDI QIDQ5408536zbMATH OpenOpenAlexFDO

Authors Patrick Cousot, Radhia Cousot, Francesco Logozzo

Publication date 10 April 2014

Published in Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1926385.1926399

zbMATH Keywords

abstract interpretationstatic analysisprogram verificationinvariant synthesisarray abstractionarray content analysisarray property inference

Mathematics Subject Classification ID

Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• An array content static analysis based on non-contiguous partitions
• Generic abstraction of dictionaries and arrays
• A scalable segmented decision tree abstract domain
• An abstract memory functor for verified C static analyzers
• Non-disjunctive Numerical Domain for Array Predicate Abstraction

Cited in

(19)

• Verifying array manipulating programs with full-program induction
• \textsc{Diffy}: inductive reasoning of array programs using difference invariants
• Generic abstraction of dictionaries and arrays
• Automaton-based array initialization analysis
• Abstraction of arrays based on non contiguous partitions
• The map equality domain
• An extension of lazy abstraction with interpolation for programs with arrays
• Data abstraction: a general framework to handle program verification of data structures
• A scalable segmented decision tree abstract domain
• FunArray
• Static contract checking with abstract interpretation
• Inferring functional properties of matrix manipulating programs by abstract interpretation
• Checking array bounds by abstract interpretation and symbolic expressions
• Analyzing Array Manipulating Programs by Program Transformation
• Precondition inference from intermittent assertions and application to contracts on collections
• Relational abstract interpretation of arrays in assembly code
• Inferring complete initialization of arrays
• Lingva: generating and proving program properties using symbol elimination
• An array content static analysis based on non-contiguous partitions

Describes a project that uses

Uses Software

• ASTREE
• Boogie
• z3
• Spec#
• Eiffel

This page was built for publication: A parametric segmentation functor for fully automatic and scalable array content analysis

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