We present an abstraction framework based on modal logic and predicate abstraction technique. In the framework we employ modal logic 2CTLN in order to express predicates for abstraction and specifications of programs. The logic has enough expressive power to describe properties of heaps, such as reachability. Moreover it fits predicate abstraction scheme because its satisfiability problem is decidable. We also present a tool MLAT, an application of the framework for heap analysis. (Source: http://dl.acm.org/)

This software is also peer reviewed by journal TOMS.