کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
4951851 1441610 2017 16 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Constraint specialisation in Horn clause verification
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Constraint specialisation in Horn clause verification
چکیده انگلیسی


- We present a program transformation for strengthening the constraints in the Horn clauses.
- The transformation uses query-answer transformation and abstract interpretation.
- We demonstrate the effectiveness of the transformation by applying it to Horn clause verification problems.

We present a method for specialising the constraints in constrained Horn clauses with respect to a goal. We use abstract interpretation to compute a model of a query-answer transformed version of a given set of clauses and a goal. The constraints from the model are then used to compute a specialised version of each clause. The effect is to propagate the constraints from the goal top-down and propagate answer constraints bottom-up. The specialisation procedure can be repeated to yield further specialisation. The approach is independent of the abstract domain and the constraint theory underlying the clauses. Experimental results on verification problems show that this is an effective transformation, both in our own verification tools (based on a convex polyhedra analyser) and as a pre-processor to other Horn clause verification tools.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 137, 1 April 2017, Pages 125-140
نویسندگان
, ,