کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
6885285 | 1444504 | 2018 | 13 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
DiVM: Model checking with LLVM and graph memory
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
شبکه های کامپیوتری و ارتباطات
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
In this paper, we introduce the concept of a virtual machine with graph-organised memory as a versatile backend for both explicit-state and abstraction-driven verification of software. Our virtual machine uses the LLVM IR as its instruction set, enriched with a small set of hypercalls. We show that the provided hypercalls are sufficient to implement a small operating system, which can then be linked with applications to provide a POSIX-compatible verification environment. Finally, we demonstrate the viability of the approach through a comparison with a more traditionally-designed LLVM model checker.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Systems and Software - Volume 143, September 2018, Pages 1-13
Journal: Journal of Systems and Software - Volume 143, September 2018, Pages 1-13
نویسندگان
Petr RoÄkai, VladimÃr Å till, Ivana Äerná, JiÅÃ Barnat,