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

چکیده انگلیسی
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
Journal: The Journal of Logic and Algebraic Programming - Volume 69, Issues 1–2, August–December 2006, Pages 75-92