An array content static analysis based on non-contiguous partitions

DOI10.1016/J.CL.2016.01.005MaRDI QIDQ681352zbMATH OpenOpenAlexFDO

Authors Jiangchao Liu, Xavier Rival

Publication date 30 January 2018

Published in Computer Languages, Systems \& Structures (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01399837/file/Liu-Rival-ComputersLanguages-2016.pdf

zbMATH Keywords

program verificationabstract domainarray analysis

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Abstraction of arrays based on non contiguous partitions
• Non-disjunctive Numerical Domain for Array Predicate Abstraction
• A parametric segmentation functor for fully automatic and scalable array content analysis
• Relational abstract interpretation of arrays in assembly code
• Generic abstraction of dictionaries and arrays

Cites work

• scientific article; zbMATH DE number 1953274 (Why is no real title available?)
• scientific article; zbMATH DE number 804400 (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
• Abstraction Refinement for Quantified Array Assertions
• Abstraction of arrays based on non contiguous partitions
• Array Abstractions from Proofs
• Constructive versions of Tarski's fixed point theorems
• Decision procedures for flat array properties
• Definability of accelerated relations in a theory of arrays and its applications
• Fluid updates: beyond strong vs. weak updates
• Grammar Analysis and Parsing by Abstract Interpretation
• Invariant Synthesis for Combined Theories
• Lifting abstract interpreters to quantified logical domains
• Precise reasoning for programs using containers
• QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers
• Reduced product combination of abstract domains for shapes
• Relational inductive shape analysis
• Scalable Shape Analysis for Systems Code
• The octagon abstract domain
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(7)

• Generic abstraction of dictionaries and arrays
• A framework for numeric analysis of array operations
• Abstraction of arrays based on non contiguous partitions
• Non-disjunctive Numerical Domain for Array Predicate Abstraction
• Lightweight shape analysis based on physical types
• A parametric segmentation functor for fully automatic and scalable array content analysis
• Relational abstract interpretation of arrays in assembly code

Describes a project that uses

Uses Software

• FunArray
• Apron

This page was built for publication: An array content static analysis based on non-contiguous partitions

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