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

DOI10.1145/1926385.1926399zbMath1284.68210OpenAlexW4230509083MaRDI QIDQ5408536

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

static analysisabstract interpretationprogram 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)

Related Items (16)

Verifying Array Manipulating Programs with Full-Program Induction ⋮ \textsc{Diffy}: inductive reasoning of array programs using difference invariants ⋮ The map equality domain ⋮ Lingva: Generating and Proving Program Properties Using Symbol Elimination ⋮ Data abstraction: a general framework to handle program verification of data structures ⋮ Inferring complete initialization of arrays ⋮ Analyzing Array Manipulating Programs by Program Transformation ⋮ Relational abstract interpretation of arrays in assembly code ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ An array content static analysis based on non-contiguous partitions ⋮ Generic Abstraction of Dictionaries and Arrays ⋮ A Scalable Segmented Decision Tree Abstract Domain ⋮ Inferring functional properties of matrix manipulating programs by abstract interpretation ⋮ Static Contract Checking with Abstract Interpretation ⋮ Precondition Inference from Intermittent Assertions and Application to Contracts on Collections ⋮ FunArray

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