21 citations · 82 across the 20 of their papers we have counts for
25 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…
Analysis and Transformation of Constrained Horn Clauses for Program Verification
Emanuele De Angelis, Fabio Fioravanti, John P. Gallagher +3
This paper surveys recent work on applying analysis and transformation techniques that originate in the field of constraint logic programming (CLP) to the problem of verifying soft…
An Experiment Combining Specialization with Abstract Interpretation
John P. Gallagher, Robert Glück
It was previously shown that control-flow refinement can be achieved by a program specializer incorporating property-based abstraction, to improve termination and complexity analys…
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…
Polyvariant Program Specialisation with Property-based Abstraction
John P. Gallagher
In this paper we show that property-based abstraction, an established technique originating in software model checking, is a flexible method of controlling polyvariance in program…
Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis
Jesús J. Doménech, John P. Gallagher, Samir Genaim
Control-flow refinement refers to program transformations whose purpose is to make implicit control-flow explicit, and is used in the context of program analysis to increase precis…