Numeric inference of heap shapes for the automated analysis of heap-allocating programs

Auteurs

• Holger Siegel

Paramètres

• Informatique, programmation

En savoir plus sur le livre

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.

Achat du livre

• Année de publication: 2016
• Reliure: (rigide)