Sep 26, 2017: Christina Jansen: Graph-based Abstract Interpretation for Pointer Programs

September 26, 2017Graph-based Abstract Interpretation for Pointer Programs
Room: Hal B 2BChristina Jansen

The automated analysis and verification of pointer-manipulating programs operating on a heap is a challenging task. It requires abstraction techniques for dealing with complex program behaviour and unbounded state spaces that arise from both dynamic data structures and recursive procedures.

In this talk I am going to present a static analysis for pointer programs, which fits into the standard abstract interpretation framework. Its abstraction and (local) concretisation functions are defined by graph grammar application, more precisely utilising hyperedge replacement grammars.

We will have a look into the prototypic analysis tool Attestor and briefly consider some case studies including list reversal, the Deutsch-Schorr-Waite tree traversal algorithm and operations on AVL tree.

Moreover I will give a glimpse on an extension of the approach featuring an interprocedural as well as thread-modular analysis.