کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
6874861 | 1441445 | 2018 | 32 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Formally verifying exceptions for low-level code with separation logic
ترجمه فارسی عنوان
به صورت رسمی استثنائات برای کد کم سطح با منطق جداسازی را تایید می کند
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
چکیده انگلیسی
Exceptions in low-level architectures are implemented as synchronous interrupts: upon the execution of a faulty instruction the processor jumps to a piece of code that handles the error. Previous work has shown that assembly programs can be written, verified and run using higher-order separation logic [14]. However, execution of faulty instructions is then specified as either being undefined or terminating with an error. In this paper, we study synchronous interrupts and show their usefulness by implementing a memory allocator. This shows that it is indeed possible to write positive specifications of programs that fault. All of our results are mechanised in the interactive proof assistant Coq.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 94, January 2018, Pages 1-14
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 94, January 2018, Pages 1-14
نویسندگان
Marco Paviotti, Jesper Bengtson,