On the verification of 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, compo...

Full description

Saved in:
Bibliographic Details
Published in:Journal of computer and system sciences 2005-11, Vol.71 (4), p.535-575
Main Authors: Gori, Roberta, Levi, Giorgio
Format: Article
Language:English
Subjects:
Abstract interpretation
Finite failure
Logic programming
Program verification
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0022-0000
1090-2724
DOI:10.1016/j.jcss.2005.06.001