کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
9657465 | 1441796 | 2005 | 18 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Generating error traces from verification-condition counterexamples
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
A technique for finding errors in computer programs is to translate a given program and its correctness criteria into a logical formula in mathematics and then let an automatic theorem prover check the validity of the formula. This approach gives the tool designer much flexibility in which conditions are to be checked, and the technique can reason about as many aspects of the given program as the underlying theorem prover allows. This paper describes a method for reconstructing, from the theorem prover's mathematical output, error traces that lead to the program errors that the theorem prover discovers.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 55, Issues 1â3, March 2005, Pages 209-226
Journal: Science of Computer Programming - Volume 55, Issues 1â3, March 2005, Pages 209-226
نویسندگان
K. Rustan M. Leino, Todd Millstein, James B. Saxe,