Monotonic Abstraction for Programs with Dynamic Memory Heaps

Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Fr\'{e}d\'{e}ric Haziza, Ahmed Rezine

We propose a new approach for automatic verification of programs with dynamic heap manipulation. The method is based on symbolic (backward) reachability analysis using upward-closed sets of heaps w.r.t. an appropriate preorder on graphs. These sets are represented by a finite set of minimal graph patterns corresponding to a set of bad configurations. We define an abstract semantics for the programs which is monotonic w.r.t. the preorder. Moreover, we prove that our analysis always terminates by showing that the preorder is a well-quasi ordering. Our results are presented for the case of programs with 1-next selector. We provide experimental results showing the effectiveness of our approach.

In Proceedings of the 20th international conference on Computer Aided Verification (CAV), 2008,

Last version (pdf) 2008