Statically inferring complex heap, array, and numeric invariants

DOI10.1007/978-3-642-15769-1_6MaRDI QIDQ4930717zbMATH OpenOpenAlexFDO

Authors Bill McCloskey, Mooly Sagiv, Thomas Reps

Publication date 1 October 2010

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-15769-1_6

Mathematics Subject Classification ID

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

Recommendations

• Automatic inference of heap properties exploiting value domains
• scientific article; zbMATH DE number 7361354
• An abstract memory functor for verified C static analyzers
• Arithmetic Strengthening for Shape Analysis
• Quantified Heap Invariants for Object-Oriented Programs

Cited in

(8)

• A divide-and-conquer approach for analysing overlaid data structures
• A generic framework for heap and value analyses of object-oriented programming languages
• Reversible Representation and Manipulation of Constructor Terms in the Heap
• Abstract domains for automated reasoning about list-manipulating programs with infinite data
• Improving Static Variable Orders Via Invariants
• Inferring complete initialization of arrays
• Quantified Heap Invariants for Object-Oriented Programs
• Automatic inference of heap properties exploiting value domains

Describes a project that uses

Uses Software

• CSSV

This page was built for publication: Statically inferring complex heap, array, and numeric invariants

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