Projekter pr. år
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 queryanswer transformation of a given set of clauses and a goal. The effect is to propagate the
constraints from the goal topdown and propagate answer constraints bottomup. 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 preprocessor to other Horn clause verification tools.
interpretation to compute a model of a queryanswer transformation of a given set of clauses and a goal. The effect is to propagate the
constraints from the goal topdown and propagate answer constraints bottomup. 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 preprocessor to other Horn clause verification tools.
Originalsprog  Engelsk 

Titel  Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM '15 
Redaktører  Kenichi Asai, Kostis Sagonas 
Antal sider  6 
Udgivelses sted  New York 
Forlag  Association for Computing Machinery 
Publikationsdato  4 jan. 2015 
Sider  8590 
ISBN (Trykt)  9781450332972 
DOI  
Status  Udgivet  4 jan. 2015 
Begivenhed  PEPM 2015  Tata Institute of Fundamental Research, Mumbai, Indien Varighed: 13 jan. 2015 → 14 jan. 2015 http://popl.mpisws.org/2015/ 
Konference
Konference  PEPM 2015 

Lokation  Tata Institute of Fundamental Research 
Land  Indien 
By  Mumbai 
Periode  13/01/2015 → 14/01/2015 
Andet  In cooperation with: POPL 2015: 42nd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages 
Internetadresse 
Projekter
 2 Afsluttet

ENTRA: WholeSystems Energy Transparency
Kafle, B.
01/10/2012 → 30/09/2015
Projekter: Projekt › Forskning

NUSA: Numeric and Symbolic Abstractions for Software Model Checking
Gallagher, J. P., Rosendahl, M. & Rhiger, M.
01/01/2011 → 31/12/2013
Projekter: Projekt › Forskning