Bishoksan Kafle

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

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

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..

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

B Kafle, JP Gallagher

Journal article  |  2017  |  Computer Languages, Systems & Structures

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