Constraint Specialisation in Horn Clause Verification
Sci. Comput. Program.(2017)
摘要
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 transformation of a given set of clauses and a goal. The effect is to propagate the constraints from the goal top-down and propagate answer constraints bottom-up. Our approach does not unfold the clauses at all; we use the constraints from the model to compute a specialised version of each clause in the program. The approach is independent of the abstract domain and the constraints theory underlying the clauses. Experimental results on verification problems show that this is an effective transformation, both in our own verification tools (convex polyhedra analyser) and as a pre-processor to other Horn clause verification tools.
更多查看译文
关键词
convex polyhedral analysis,abstract interpretation,specifying and verifying and reasoning about programs,query-answer transformation,horn clauses,constraint specialisation,logic programming
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络