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

DOI10.1145/1926385.1926399zbMATH Open1284.68210OpenAlexW4230509083MaRDI QIDQ5408536FDOQ5408536

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

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

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)

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
• Static contract checking with abstract interpretation
• FunArray
• 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

Uses Software

• Eiffel
• Spec#
• z3
• Boogie
• ASTREE

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)