Yoshinori Tanabe, Toshinori Takai, Toshifusa Sekizawa, Koichi Takahashi:
Preconditions of properties described in CTL for statements
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.
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