21 citations · 41 across the 11 of their papers we have counts for
14 papers
Regular Path Clauses and Their Application in Solving Loops
Bishoksan Kafle, John P. Gallagher, Manuel V. Hermenegildo +3
A well-established approach to reasoning about loops during program analysis is to capture the effect of a loop by extracting recurrences from the loop; these express relationships…
Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis
Hossein Hojjat, Bishoksan Kafle
This volume contains the post-proceedings of the 8th Workshop on Horn Clauses for Verification and Synthesis (HCVS), which took place virtually due to Covid-19 pandemic as an affil…
Transformation-Enabled Precondition Inference
Bishoksan Kafle, Graeme Gange, Peter J. Stuckey +2
Precondition inference is a non-trivial problem with important applications in program analysis and verification. We present a novel iterative method for automatically deriving pre…
From Big-Step to Small-Step Semantics and Back with Interpreter Specialisation
John P. Gallagher, Manuel Hermenegildo, Bishoksan Kafle +3
We investigate representations of imperative programs as constrained Horn clauses. Starting from operational semantics transition rules, we proceed by writing interpreters as const…
Precondition Inference via Partitioning of Initial States
Bishoksan Kafle, Graeme Gange, Peter Schachte +2
Precondition inference is a non-trivial task with several applications in program analysis and verification. We present a novel iterative method for automatically deriving sufficie…
An iterative approach to precondition inference using constrained Horn clauses
Bishoksan Kafle, John P. Gallagher, Graeme Gange +3
We present a method for automatic inference of conditions on the initial states of a program that guarantee that the safety assertions in the program are not violated. Constrained…
Tree dimension in verification of constrained Horn clauses
Bishoksan Kafle, John P. Gallagher, Pierre Ganty
In this paper, we show how the notion of tree dimension can be used in the verification of constrained Horn clauses (CHCs). The dimension of a tree is a numerical measure of its br…
Solving non-linear Horn clauses using a linear Horn clause solver
Bishoksan Kafle, John P. Gallagher, Pierre Ganty
In this paper we show that checking satisfiability of a set of non-linear Horn clauses (also called a non-linear Horn clause program) can be achieved using a solver for linear Horn…
ENTRA: Whole-Systems Energy Transparency
Kerstin Eder, John P. Gallagher, Pedro Lopez-Garcia +14
Promoting energy efficiency to a first class system design goal is an important research challenge. Although more energy-efficient hardware can be designed, it is software that con…
Interpolant Tree Automata and their Application in Horn Clause Verification
Bishoksan Kafle, John P. Gallagher
This paper investigates the combination of abstract interpretation over the domain of convex polyhedra with interpolant tree automata, in an abstraction-refinement scheme for Horn…
Decomposition by tree dimension in Horn clause verification
Bishoksan Kafle, John P. Gallagher, Pierre Ganty
In this paper we investigate the use of the concept of tree dimension in Horn clause analysis and verification. The dimension of a tree is a measure of its non-linearity - for exam…
Solving non-linear Horn clauses using a linear solver
Bishoksan Kafle
Developing an efficient non-linear Horn clause solver is a challenging task since the solver has to reason about the tree structures rather than the linear ones as in a linear solv…
Optimised determinisation and completion of finite tree automata
John P. Gallagher, Mai Ajspur, Bishoksan Kafle
Determinisation and completion of finite tree automata are important operations with applications in program analysis and verification. However, the complexity of the classical pro…
Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification
Bishoksan Kafle, John P. Gallagher
We present an approach to constrained Horn clause (CHC) verification combining three techniques: abstract interpretation over a domain of convex polyhedra, specialisation of the co…