Title
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
Abstract
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.
Files
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