Yoshinori Tanabe, Toshinori Takai, Toshifusa Sekizawa, Koichi Takahashi: Preconditions of properties described in CTL for statements manipulating pointers. Supplemental Volume of the 2005 International Conference on Dependable Systems and Networks, June 28-July 1, 2005, pp.228-234


In the predicate abstraction framework for verification, two key issues are computation of the weakest precondition of a predicate and decision procedure of satisfiability checking of predicates. We propose to use temporal formulas as predicate for verifying properties on structures with pointers. In this paper we report that the first issue has been solved for CTL formulas.


Slides Previous versions:

This page is a part of the web site of National Institute of Advanced Industrial Science and Technology (AIST) .

Contact for contents of this page:: tanabe.yoshinori (atmark) aist.go.jp

Home of Tanabe's page