Constraint Specialisation in Horn Clause Verification

Bishoksan Kafle, John Patrick Gallagher

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

Abstract

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.
OriginalsprogEngelsk
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
Sider85-90
ISBN (Trykt)978-1-4503-3297-2
DOI
StatusUdgivet - 4 jan. 2015
BegivenhedPEPM 2015 - Tata Institute of Fundamental Research, Mumbai, Indien
Varighed: 13 jan. 201514 jan. 2015
http://popl.mpi-sws.org/2015/

Konference

KonferencePEPM 2015
LokationTata Institute of Fundamental Research
LandIndien
ByMumbai
Periode13/01/201514/01/2015
AndetIn cooperation with: POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Internetadresse

Citer dette