Constraint Specialisation in Horn Clause Verification

Bishoksan Kafle, John Patrick Gallagher

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review


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.
TitelProceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15
RedaktørerKenichi Asai, Kostis Sagonas
Antal sider6
Udgivelses stedNew York
ForlagAssociation for Computing Machinery
Publikationsdato4 jan. 2015
ISBN (Trykt)978-1-4503-3297-2
StatusUdgivet - 4 jan. 2015
BegivenhedPEPM 2015 - Tata Institute of Fundamental Research, Mumbai, Indien
Varighed: 13 jan. 201514 jan. 2015


KonferencePEPM 2015
LokationTata Institute of Fundamental Research
AndetIn cooperation with: POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Citer dette