کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
9655913 | 685223 | 2005 | 12 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Decision Procedures for Set-Valued Fields
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
![عکس صفحه اول مقاله: Decision Procedures for Set-Valued Fields Decision Procedures for Set-Valued Fields](/preview/png/9655913.png)
چکیده انگلیسی
In this paper we explore reasoning techniques for programs that manipulate data structures specified using set-valued abstract fields associated with container objects. We compare the expressive power and the complexity of specification languages based on 1) decidable prefix vocabulary classes of first-order logic, 2) two-variable logic with counting, and 3) Nelson-Oppen combinations of multisorted theories. Such specification logics can be used for verification of object-oriented programs with supplied invariants. Moreover, by selecting an appropriate subset of properties expressible in such logic, the decision procedures for these logics enable automated computation of lattice operations in an abstract interpretation domain, as well as automated computation of abstract program semantics.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 131, 24 May 2005, Pages 51-62
Journal: Electronic Notes in Theoretical Computer Science - Volume 131, 24 May 2005, Pages 51-62
نویسندگان
Viktor Kuncak, Martin Rinard,