Automatic numeric abstractions for heap-manipulating programs

DOI10.1145/1706299.1706326MaRDI QIDQ5255075zbMATH OpenOpenAlexWikidataFDO

Authors

Publication date 11 June 2015

Published in Proceedings of the 37th 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/1706299.1706326

zbMATH Keywords

abstractionprogram verificationseparation logicshape analysistermination

Mathematics Subject Classification ID

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

Recommendations

• Verification, Model Checking, and Abstract Interpretation
• Monotonic Abstraction for Programs with Dynamic Memory Heaps
• An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps
• Abstract domains for automated reasoning about list-manipulating programs with infinite data

Cited in

(21)

• Recognition of logically related regions based heap abstraction
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Complexity and resource bound analysis of imperative programs using difference constraints
• A generic framework for heap and value analyses of object-oriented programming languages
• Invariants synthesis over a combined domain for automated program verification
• Abstract domains for automated reasoning about list-manipulating programs with infinite data
• Counterexample validation and interpolation-based refinement for forest automata
• Verification of heap manipulating programs with ordered data by extended forest automata
• Relational decomposition
• Generating abstract graph-based procedure summaries for pointer programs
• Disproving inductive entailments in separation logic via base pair approximation
• Heap Assumptions on Demand
• Monotonic Abstraction for Programs with Dynamic Memory Heaps
• Reasoning about heap manipulating programs using automata techniques
• Automatic inference of heap properties exploiting value domains
• A semantics for procedure local heaps and its abstractions
• An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software
• Ranking functions for linear-constraint loops
• Verification, Model Checking, and Abstract Interpretation
• Automatically verifying temporal properties of pointer programs with cyclic proof
• Termination analysis of programs with multiphase control-flow

This page was built for publication: Automatic numeric abstractions for heap-manipulating programs

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