7 citations · 8 across the 3 of their papers we have counts for
6 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…
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…