Numeric Inference of Heap Shapes for the Automated Analysis of Heap-Allocating Programs

Beschreibung

This thesis presents a novel approach to the analysis of heap-allocating programs that is based solely on abstract numeric domains. In contrast to approaches that require the user to provide so-called instrumentation predicates, our analysis is geared towards the automatic inference of heap invariants. Using off-the-shelf relational numeric domains, we infer invariants that relate the shape of heap-allocated data structures to their numeric content. Our analysis is implemented as a stack of functor domains and is shown to be able to infer invariants that distinguish between lists, trees and arbitrary graphs, thereby allowing for the automatic verification of standard algorithms.

Autor*in

Holger Siegel

Themen in »Numeric Inference of Heap Shapes for the Automated Analysis of Heap-Allocating Programs«

Heap Shapes Heap-Allocating Programs Numeric Inference

Stimmen zu »Numeric Inference of Heap Shapes for the Automated Analysis of Heap-Allocating Programs«

Details

Link teilen