کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
10333012 688167 2005 41 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
On the verification of finite failure
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
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, 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.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Computer and System Sciences - Volume 71, Issue 4, November 2005, Pages 535-575
نویسندگان
, ,