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

DOI10.1007/978-3-540-73368-3_42zbMATH Open1135.68366OpenAlexW1553910098MaRDI QIDQ5429331FDOQ5429331

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

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

Mathematics Subject Classification ID

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

Cited In (10)

• Quantified Heap Invariants for Object-Oriented Programs
• Region Analysis for Race Detection
• Quantitative separation logic and programs with lists
• A generic framework for heap and value analyses of object-oriented programming languages
• The map equality domain
• Verification, Model Checking, and Abstract Interpretation
• A Reachability Predicate for Analyzing Low-Level Software
• 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)