20 citations · 26 across the 7 of their papers we have counts for
8 papers
Teaching Simple Constructive Proofs with Haskell Programs
Matthew Farrugia-Roberts, Bryn Jeffries, Harald Søndergaard
In recent years we have explored using Haskell alongside a traditional mathematical formalism in our large-enrolment university course on topics including logic and formal language…
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…
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…
Horn Clauses as an Intermediate Representation for Program Analysis and Transformation
Graeme Gange, Jorge A. Navas, Peter Schachte +2
Many recent analyses for conventional imperative programs begin by transforming programs into logic programs, capitalising on existing LP analyses and simple LP semantics. We propo…
A Complete Refinement Procedure for Regular Separability of Context-Free Languages
Graeme Gange, Jorge A. Navas, Peter Schachte +2
Often, when analyzing the behaviour of systems modelled as context-free languages, we wish to know if two languages overlap. To this end, we present an effective semi-decision proc…
A Partial-Order Approach to Array Content Analysis
Graeme Gange, Jorge A. Navas, Peter Schachte +2
We present a parametric abstract domain for array content analysis. The method maintains invariants for contiguous regions of the array, similar to the methods of Gopan, Reps and S…
Binary Decision Diagrams for Affine Approximation
Kevin Henshall, Peter Schachte, Harald Søndergaard +1
Selman and Kautz's work on ``knowledge compilation'' established how approximation (strengthening and/or weakening) of a propositional knowledge-base can be used to speed up query…