On the verification of finite failure

作     者：Gori, R Levi, G 

作者机构：Univ Pisa Dipartimento Informat I-56127 Pisa Italy 

出 版 物：《JOURNAL OF COMPUTER AND SYSTEM SCIENCES》 (计算机与系统科学杂志)

年 卷 期：2005年第71卷第4期

页      面：535-575页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：abstract interpretation logic programming program verification finite failure 

摘      要：In Gori [An abstract interpretation framework to reason on finite failure and other properties of finite and infinite computations, Theoret. Comput. Sci. 290(1) (2003) 863-936] a new fixpoint semantics which correctly models finite failure has been defined. This semantics is And-compositional, compositional w.r.t. instantiation and is based on a co-continuous operator. Based on this fixpoint semantics a new inductive method able to verify a program w.r.t. the property of finite failure can be defined. In this paper we show how Ferrand s approach, using both a least fixpoint and greatest fixpoint semantics, can be adapted to finite failure. The verification method is not effective. Therefore, we consider an approximation from above and an approximation from below of our semantics, which give two different finite approximations. These approximations are used for effective program verification. (c) 2005 Elsevier Inc. All rights reserved.