T. Sekizawa, Y. Tanabe, Y. Yuasa, and K. Takahashi (Japan)
Verification, Predicate Abstraction, Heap Analysis, Modal Logic
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 predi cates 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 de cidable. We also present a tool MLAT, an application of the framework for heap analysis.
Important Links:
Go Back
