An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software

DOI10.1007/978-3-540-73368-3_42MaRDI QIDQ5429331zbMATH OpenOpenAlexFDO

Authors Sumit Gulwani, Ashish Tiwari

Publication date 29 November 2007

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73368-3_42

Mathematics Subject Classification ID

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

Recommendations

• Verification, Model Checking, and Abstract Interpretation
• Automatic numeric abstractions for heap-manipulating programs
• Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
• A Reachability Predicate for Analyzing Low-Level Software
• Automatic inference of heap properties exploiting value domains

Cited in

(14)

• Quantified Heap Invariants for Object-Oriented Programs
• From low-level pointers to high-level containers
• Quantitative separation logic and programs with lists
• A generic framework for heap and value analyses of object-oriented programming languages
• Region Analysis for Race Detection
• Automatic numeric abstractions for heap-manipulating programs
• The map equality domain
• Verification, Model Checking, and Abstract Interpretation
• A Reachability Predicate for Analyzing Low-Level Software
• Abstract domains for automated reasoning about list-manipulating programs with infinite data
• Automatic inference of heap properties exploiting value domains
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Hierarchical shape abstraction for analysis of free list memory allocators
• Interprocedural Shape Analysis with Separated Heap Abstractions

This page was built for publication: An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software

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