کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
433364 1441674 2014 29 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Backward under-approximations in numeric abstract domains to automatically infer sufficient program conditions
ترجمه فارسی عنوان
کم زیر مقادیر عقب در حوزه های انتزاعی عددی به طور خودکار شرایط برنامه کافی را به دست می آورند
کلمات کلیدی
تفسیر چکیده، تحلیل برگشتی، دامنه های انتزاعی عددی، تجزیه و تحلیل استاتیک، زیر تقریبی
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
چکیده انگلیسی


• We automatically compute sufficient conditions for program correctness.
• We rely on Abstract Interpretation to compute sound approximate solutions.
• We present under-approximations for existing numeric abstract domains.
• We built a (freely available) prototype implementation using polyhedra.

In this article, we discuss the automatic inference of sufficient preconditions by abstract interpretation and sketch the construction of an under-approximating backward analysis. We focus on numeric properties of variables and revisit three classic numeric abstract domains: intervals, octagons, and polyhedra, with new under-approximating backward transfer functions, including the support for non-deterministic expressions, as well as lower widenings to handle loops. We show that effective under-approximation is possible natively in these domains without necessarily resorting to disjunctive completion nor domain complementation. Applications include the derivation of sufficient conditions for a program to never step outside an envelope of safe states, or dually to force it to eventually fail. We built a proof-of-concept prototype implementation and tried it on simple examples. Our construction and our implementation are very preliminary and mostly untried; our hope is to convince the reader that this constitutes a worthy avenue of research.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 93, Part B, 1 November 2014, Pages 154–182
نویسندگان
,