کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
431231 1441293 2006 18 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Verifying an infinite systolic algorithm using third-order equational methods
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Verifying an infinite systolic algorithm using third-order equational methods
چکیده انگلیسی

We consider using third-order equational methods to formally verify that an infinite systolic algorithm correctly implements a family of convolution functions. The detailed case study we present illustrates the use of third-order algebra as a formal framework for developing families of computing systems. It also provides an interesting insight into the use of infinite algorithms as a means of verifying a family of finite algorithms. We consider using purely equational reasoning in our verification proofs and in particular, using the rule of free variable induction. We conclude by considering how our verification proofs can be automated using rewriting techniques.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: The Journal of Logic and Algebraic Programming - Volume 69, Issues 1–2, August–December 2006, Pages 75-92