کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
422501 | 685095 | 2007 | 18 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Extracting Program Logics From Abstract Interpretations Defined by Logical Relations
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
We connect the activity of defining an abstract-interpretation-based static analysis with synthesizing its appropriate programming logic by applying logical relations as demonstrated by Abramsky. We begin with approximation relations of base type, which relate concrete computational values to their approximations, and we lift the relations to function space and upper- and lower-powerset. The resulting family's properties let us synthesize an appropriate logic for reasoning about the outcome of a static analysis. The relations need not generate Galois connections, but when they do, we show that the relational notions of soundness and completeness coincide with the Galois-connection-based notions.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 173, 2 April 2007, Pages 339-356
Journal: Electronic Notes in Theoretical Computer Science - Volume 173, 2 April 2007, Pages 339-356