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

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

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)

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

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)