Bishoksan Kafle

Regular path clauses and their application in solving loops

B Kafle, JP Gallagher, MV Hermenegildo, M Klemen, P López-García, JF Morales

Journal article  |  2021  |  Electronic Proceedings in Theoretical Computer Science, EPTCS

A well-established approach to reasoning about loops during program analysis is to capture the effect of a loop by extracting recu..

Transformation-Enabled Precondition Inference

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

Journal article  |  2021  |  Theory and Practice of Logic Programming

Precondition inference is a non-trivial problem with important applications in program analysis and verification. We present a nov..

From big-step to small-step semantics and back with interpreter specialisation

JP Gallagher, M Hermenegildo, B Kafle, M Klemen, PL García, J Morales

Conference Proceedings  |  2020  |  Electronic Proceedings in Theoretical Computer Science, EPTCS

We investigate representations of imperative programs as constrained Horn clauses. Starting from operational semantics transition ..

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

We present a method for automatic inference of conditions on the initial states of a program that guarantee that the safety assert..

Tree dimension in verification of constrained Horn clauses

B Kafle, JP Gallagher, P Ganty

Journal article  |  2018  |  Theory and Practice of Logic Programming

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

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

Determinisation and completion of finite tree automata are important operations with applications in program analysis and verifica..

Constraint specialisation in Horn clause verification

Bishoksan Kafle, John P Gallagher

Journal article  |  2017  |  SCIENCE OF COMPUTER PROGRAMMING

We present a method for specialising the constraints in constrained Horn clauses with respect to a goal. We use abstract interpret..

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

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

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

B Kafle, JP Gallagher

Journal article  |  2017  |  Computer Languages, Systems and Structures

In this paper we apply tree-automata techniques to refinement of abstract interpretation in Horn clause verification. We go beyond..

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

Promoting energy efficiency to a first class system design goal is an important research challenge. Although more energy-efficient..