Bishoksan Kafle

An iterative approach to precondition inference using constrained Horn clauses

Bishoksan Kafle, John P Gallagher, Graeme Gange, Peter Schachte, Harald Sondergaard, Peter J Stuckey

Journal article  |  2018  |  Theory and Practice of Logic Programming

Tree dimension in verification of constrained Horn clauses

B Kafle, JP Gallagher, P Ganty

Journal article  |  2018  |  Theory and Practice of Logic Programming

AbstractIn this paper, we show how the notion of tree dimension can be used in the verification of constrained Horn clauses (CHCs)..

Optimised determinisation and completion of finite tree automata

JP Gallagher, M Ajspur, B Kafle

Journal article  |  2018  |  Journal of Logical and Algebraic Methods in Programming

Constraint specialisation in Horn clause verification

Bishoksan Kafle, John P Gallagher

Journal article  |  2017  |  Science of Computer Programming

Horn clause verification with convex polyhedral abstraction and tree automata-based refinement

B Kafle, JP Gallagher

Journal article  |  2017  |  Computer Languages, Systems & Structures

A benders decomposition approach to deciding modular linear integer arithmetic

B Kafle, G Gange, P Schachte, H Søndergaard, PJ Stuckey

Conference Proceedings  |  2017  |  Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

© Springer International Publishing AG 2017. Verification tasks frequently require deciding systems of linear constraints over mod..

ENTRA: Whole-systems energy transparency

K Eder, JP Gallagher, P López-García, H Muller, Z Banković, K Georgiou, R Haemmerlé, MV Hermenegildo, B Kafle, S Kerrison, M Kirkeby, M Klemen, X Li, U Liqat, J Morse, M Rhiger, M Rosendahl

Journal article  |  2016  |  Microprocessors and Microsystems

Interpolant tree automata and their application in Horn clause verification

B Kafle, JP Gallagher

Conference Proceedings  |  2016  |  Electronic Proceedings in Theoretical Computer Science

Solving non-linear Horn clauses using a linear Horn clause solver

B Kafle, JP Gallagher, P Ganty

Conference Proceedings  |  2016  |  Electronic Proceedings in Theoretical Computer Science

RAHFT: A tool for verifying horn clauses using abstract interpretation and finite tree automata

B Kafle, JP Gallagher, JF Morales

Conference Proceedings  |  2016  |  Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

© Springer International Publishing Switzerland 2016. We present Rahft (Refinement of Abstraction in Horn clauses using Finite Tre..

Decomposition by tree dimension in Horn clause verification

B Kafle, JP Gallagher, P Ganty

Conference Proceedings  |  2015  |  Electronic Proceedings in Theoretical Computer Science

Constraint specialisation in horn clause verification

B Kafle, JP Gallagher

Conference Proceedings  |  2015  |  Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation - PEPM '15

© 2015 ACM. We present a method for specialising the constraints in constrained Horn clauses with respect to a goal. We use abstra..

Tree automata-based refinement with application to horn clause verification

B Kafle, JP Gallagher

Conference Proceedings  |  2015  |  Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

© Springer-Verlag Berlin Heidelberg 2015. In this paper we apply tree-automata techniques to refinement of abstract interpretation..

Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification

J Gallagher, K Bishoksan

Conference Proceedings  |  2014  |  Electronic Proceedings in Theoretical Computer Science

We present an approach to constrained Horn clause (CHC) verification combining three techniques: abstract interpretation over a do..