Publications by Prof Andy King

ISO Prolog provides catch and throw to realise the control flow of exception handling. This pearl demonstrates that catch and throw are inconspicuously amenable to the implementation of backjumping. In fact, they have precisely the semantics required: rewinding the search to a specific point, and carrying of a preserved term to that point. The utility of these properties is demonstrated through an implementation of graph colouring with backjumping and a backjumping SAT solver that applies Conflict Driven Clause Learning.

The octagon abstract domain is a widely used numeric abstract domain expressing relational information between variables whilst being both computationally efficient and simple to implement. Each element of the domain is a system of constraints where each constraint takes the restricted form ±xi±xj≤c. A key family of operations for the octagon domain are closure algorithms, which check satisfiability and provide a normal form for octagonal constraint systems. We present new quadratic incremental algorithms for closure, strong closure and integer closure and proofs of their correctness. We highlight the benefits and measure the performance of these new algorithms.

Subclasses of linear inequalities where each inequality has at most two variables are popular in abstract interpretation and model checking, because they strike a balance between what can be described and what can be efficiently computed. This paper focuses on the TVPI class of inequalities, for which each coefficient of each two variable inequality is unrestricted. An implied TVPI inequality can be generated from a pair of TVPI inequalities by eliminating a given common variable (echoing resolution on clauses). This operation, called result, can be applied to derive TVPI inequalities which are entailed (implied) by a given TVPI system. The key operation on TVPI is calculating closure: satisfiability can be observed from a closed system and a closed system also simplifies the calculation of other operations. A closed system can be derived by repeatedly applying the result operator. The process of adding a single TVPI inequality to an already closed input TVPI system and then finding the closure of this augmented system is called incremental closure. This too can be calculated by the repeated application of the result operator. This paper studies the calculus defined by result, the structure of result derivations, and how derivations can be combined and controlled. A series of lemmata on derivations are presented that, collectively, provide a pathway for synthesising an algorithm for incremental closure. The complexity of the incremental closure algorithm is analysed and found to be O((n^2+m^2)lg(m)), where n is the number of variables and $m$ the number of inequalities of the input TVPI system.

Although it is agreed that the Volgenant-Jonker (VJ) algorithm provides a fast way to approximate graph edit distance (GED), until now nobody has reported how the VJ algorithm can be tuned for this task. To this end, we revisit VJ and propose a series of refinements that improve both the speed and memory footprint without sacrificing accuracy in the GED approximation. We quantify the effectiveness of these optimisations by measuring distortion between control-flow graphs: a problem that arises in malware matching. We also document an unexpected behavioural property of VJ in which the time required to find shortest paths to unassigned vertices decreases as graph size increases, and explain how this phenomenon relates to the birthday paradox.

The fact that Java is platform independent gives hackers the opportunity to write exploits that can target users on any platform, which has a JVM implementation. Metasploit is a well-known source of Javaexploits and to circumvent detection by Anti Virus (AV) software, obfuscation techniques are routinely applied to make an exploit more difficult to recognise. Popular obfuscation techniques for Java include stringobfuscation and applying reflection to hide method calls; two techniques that can either be used together or independently. This paper shows how to apply partial evaluation to remove these obfuscations and thereby improve AV matching. The paper presents a partial evaluator for Jimple, which is an intermediate language for JVM bytecode designed for optimisation and program analysis, and demonstrates how partially evaluated Jimple code, when transformed back into Java, improves the detection rates of a number of commercial AV products.

SAT Modulo Theories (SMT) is the problem of determining the satisfiability of a formula in which constraints, drawn from a given constraint theory T, are composed with logical connectives. The DPLL(T) approach to SMT has risen to prominence as a technique for solving these quantifier-free problems. The key idea in DPLL(T) is to couple unit propagation in the propositional part of the problem with theory propagation in the constraint component. In this paper it is demonstrated how reification provides a natural way for orchestrating this in the setting of logic programming. This allows an elegant implementation of DPLL(T) solvers in Prolog. The work is motivated by a problem in reverse engineering, that of type recovery from binaries. The solution to this problem requires an SMT solver where the theory is that of rational-tree constraints, a theory not supported in off-the-shelf SMT solvers, but realised as unification in Prolog systems. The approach is also illustrated with SMT solvers for linear constraints and integer difference constraints. The rational-tree solver is benchmarked against a number of type recovery problems, and compared against a lazy-basic SMT solver built on PicoSAT, while the integer difference logic solver is benchmarked against CVC3 and CVC4, both of which are implemented in C++.

Bitwise instructions, loops and indirect data access present challenges to the verification of microcontroller programs. In particular, since registers are often memory mapped, it is necessary to show that an indirect store operation does not accidently mutate a register. To prove this and related properties, this article advocates using the domain of bit-wise linear congruences in conjunction with intervals to derive accurate range information. The paper argues that these two domains complement one another when reasoning about microcontroller code. The paper also explains how SAT solving, which applied with dichotomic search, can be used to recover branching conditions from binary code which, in turn, further improves interval analysis.

Symbolic decision trees are not the only way to correlate the relationship between flags and numeric variables. Boolean formulae can also represent such relationships where the integer variables are modelled with bit-vectors of propositional variables. Boolean formulae can be composed to express the semantics of a block and program state, but they are hardly tractable, hence the need to compute their abstractions. This paper shows how incremental SAT can be applied to derive range and set abstractions for bit-vectors that are constrained by Boolean formulae.

Traditionally, transfer functions have been designed manually for each operation in a program, instruction by instruction. In such a setting, a transfer function describes the semantics of a single instruction, detailing how a given abstract input state is mapped to an abstract output state. The net effect of a sequence of instructions, a basic block, can then be calculated by composing the transfer functions of the constituent instructions. However, precision can be improved by applying a single transfer function that captures the semantics of the block as a whole. Since blocks are program-dependent, this approach necessitates automation. There has thus been growing interest in computing transfer functions automatically, most notably using techniques based on quantifier elimination. Although conceptually elegant, quantifier elimination inevitably induces a computational bottleneck, which limits the applicability of these methods to small blocks. This paper contributes a method for calculating transfer functions that finesses quantifier elimination altogether, and can thus be seen as a response to this problem. The practicality of the method is demonstrated by generating transfer functions for input and output states that are described by linear template constraints, which include intervals and octagons.

A succinct SAT solver is presented that exploits the control provided by delay declarations to implement watched literals and unit propagation. Despite its brevity the solver is surprisingly powerful and its elegant use of Prolog constructs is presented as a programming pearl. Furthermore, the SAT solver can be integrated into an SMT framework which exploits the constraint solvers that are available in many Prolog systems.

The analysis of executables is concerned with extracting information from a binary program typically, though not exclusively, with program analysis techniques based on abstract interpretation. This topic has risen to prominence due to the need to audit code, developed by third parties for which the source is unavailable. Moreover, compilers are themselves a source of bugs, hence the need to scrutinise and systematically examine executables.

This paper revisits the problem of determinacy inference addressing the problem of how to uniformly handle cut. To this end a new semantics is introduced for cut, which is abstracted to systematically derive a backward analysis that derives conditions sufficient for a goal to succeed at most once. The method is conceptionally simpler and easier to implement than existing techniques, whilst improving the latter's handling of cut. Formal arguments substantiate correctness and experimental work, and a tool called 'RedAlert' demonstrates the method's generality and applicability.

Extended abstract for Association of Logic Programming (ALP) Newsletter on FLOPS/TCS special issue paper on SAT and SMT solving in Prolog.

Quadtrees have proved popular in computer graphics and spatial databases as a way of representing regions in two dimensional space. This hierarchical data-structure is flexible enough to support non-convex and even disconnected regions, therefore it is natural to ask whether this data-structure can form the basis of an abstract domain. This paper explores this question and suggests that quadtrees offer a new approach to weakly relation domains whilst their hierarchical structure naturally lends itself to representation with boolean functions.

This article presents the Two Variable Per Inequality abstract domain (TVPI domain for short). This so-called weakly-relational domain is able to express systems of linear inequalities where each inequality has at most two variables. The domain represents a sweet-point in the performance-cost tradeoff between the faster Octagon domain and the more expressive domain of general convex polyhedra. In particular, we detail techniques to closely approximate integral TVPI systems, thereby finessing the problem of excessively growing coefficients, yielding -- to our knowledge -- the only relational domain that combines linear relations with arbitrary coefficients and strongly polynomial performance.

A logic program consists of a logic component and a control component. The former is a specification in predicate logic whereas the latter defines the order of subgoal selection. The order of subgoal selection is often controlled with delay declarations that specify that a subgoal is to suspend until some condition on its arguments is satisfied. Reasoning about delay declarations is notoriously difficult for the programmer and it is not unusual for a program and a goal to reduce to a state that contains a subgoal that suspends indefinitely. Suspending subgoals are usually unintended and often indicate an error in the logic or the control. A number of abstract interpretation schemes have therefore been proposed for checking that a given program and goal cannot reduce to such a state. This article considers a reversal of this problem, advocating an analysis that for a given program infers a class of goals that do not lead to suspension. This article shows that this more general approach can have computational, implementational and user-interface advantages. In terms of user-interface, this approach leads to a lightweight point-and-click mode of operation in which, after directing the analyser at a file, the user merely has to inspect the results inferred by the analysis. In terms of implementation, the analysis can be straightforwardly realized as two simple fixpoint computations. In terms of computation, by modeling n! different schedulings of n subgoals with a single Boolean function, it is possible to reason about the suspension behavior of large programs. In particular, the analysis is fast enough to be applied repeatedly within the program development cycle. The article also demonstrates that the method is precise enough to locate bugs in existing programs.

Detecting symmetries has many applications in logic synthesis that include, amongst other things, technology mapping, deciding equivalence of Boolean functions when the input correspondence is unknown and finding support-reducing bound sets. Mishchenko showed how to efficiently detect symmetries in ROBDDs without the need for checking equivalence of all co-factor pairs. This work resulted in practical algorithms for detecting classical and generalized symmetries. Both the classical and generalized symmetry detection algorithms are monolithic in the sense that they only return a meaningful answer when they are left to run to completion. In this paper we present anytime algorithms for detecting both classical and generalized symmetries, that output pairs of symmetric variables until a prescribed time bound is exceeded. These anytime algorithms are complete in that given sufficient time they are guaranteed to find all symmetric pairs. Anytime generality is not gained at the expense of efficiency since this approach requires only very modest data structure support and offers unique opportunities for optimization so the resulting algorithms are competitive with their monolithic counterparts.

The objective of control generation in logic programming is to derive a computation rule for a program that is efficient and yet does not compromise program correctness. Progress in solving this fundamental problem in logic programming has been slow and, to date, only partial solutions have been proposed. Previously proposed schemes are either inefficient, incomplete (incorrect) or difficult to apply for programs consisting of many components (the scheme is not modular). This paper shows how the control generation problem can be tackled by program transformation. The transformation relies on information about the depths of derivations to derive delay declarations which orchestrate the control. To prove correctness of the transformation, the notion of semi-delay recurrency is introduced, which generalises previous ideas in the termination literature for reasoning about logic programs with delay declarations. In contrast to previous work, semi-delay recurrency does not require an atom to be completely resolved before another is selected for reduction. This enhancement permits the transformation to introduce control which is flexible and relatively efficient.

A programming tactic involving polyhedra is reported that has been widely applied in the polyhedral analysis of (constraint) logic programs. The method enables the computations of convex hulls that are required for polyhedral analysis to be coded with linear constraint solving machinery that is available in many Prolog systems.

In order to improve precision and efficiency sharing analysis should track both freeness and linearity. The abstract unification algorithms for these combined domains are suboptimal, hence there is scope for improving precision. This paper proposes three optimisations for tracing sharing in combination with freeness and linearity. A novel connection between equations and sharing abstractions is used to establish correctness of these optimisations even in the presence of rational trees. A method for pruning intermediate sharing abstractions to improve efficiency is also proposed. The optimisations are lightweight and therefore some, if not all, of these optimisations will be of interest to the implementor.

Boolean functions can be used to express the groundness of, and trace grounding dependencies between, program variables in (constraint) logic programs. In this paper, a variety of issues pertaining to the efficient Prolog implementation of groundness analysis are investigated, focusing on the domain of definite Boolean functions, Def. The systematic design of the representation of an abstract domain is discussed in relation to its impact on the algorithmic complexity of the domain operations; the most frequently called operations should be the most lightweight. This methodology is applied to Def, resulting in a new representation, together with new algorithms for its domain operations utilising previously unexploited properties of Def -- for instance, quadratic-time entailment checking. The iteration strategy driving the analysis is also discussed and a simple, but very effective, optimisation of induced magic is described. The analysis can be implemented straightforwardly in Prolog and the use of a non-ground representation results in an efficient, scalable tool which does not require widening to be invoked, even on the largest benchmarks. An extensive experimental evaluation is given.

One recurring problem in program development is that of understanding how to re-use code developed by a third party. In the context of (constraint) logic programming, part of this problem reduces to figuring out how to query a program. If the logic program does not come with any documentation, then the programmer is forced to either experiment with queries in an ad hoc fashion or trace the control-flow of the program (backward) to infer the modes in which a predicate must be called so as to avoid an instantiation error. This paper presents an abstract interpretation scheme that automates the latter technique. The analysis presented in this paper can infer moding properties which if satisfied by the initial query, come with the guarantee that the program and query can never generate any moding or instantiation errors. Other applications of the analysis are discussed. The paper explains how abstract domains with certain computational properties (they condense) can be used to trace control-flow backward (right-to-left) to infer useful properties of initial queries. A correctness argument is presented and an implementation is reported.

We present verification methods for logic programs with delay declarations. The verified properties are termination and freedom from errors related to built-ins. Concerning termination, we present two approaches. The first approach tries to eliminate the well-known problem of speculative output bindings. The second approach is based on identifying the predicates for which the textual position of an atom using this predicate is irrelevant with respect to termination. Three features are distinctive of this work: it allows for predicates to be used in several modes; it shows that block declarations, which are a very simple delay construct, are sufficient to ensure the desired properties; it takes the selection rule into account, assuming it to be as in most Prolog implementations. The methods can be used to verify existing programs and assist in writing new programs.

Sharing information is useful in specialising, optimising and parallelising logic programs and thus sharing analysis is an important topic of both abstract interpretation and logic programming. Sharing analyses infer which pairs of program variables can never be bound to terms that contain a common variable. We generalise a classic pair sharing analysis from Herbrand unification to trace sharing over rational tree constraints. This is useful for reasoning about programs written in SICStus and Prolog-III because these languages use rational tree unification as the default equation solver.

The domain of positive Boolean functions, Pos, is by now well established for the analysis of the variable dependencies that arise within logic programs. Analyses based on Pos that use binary decision diagrams have been shown to be efficient for a wide range of practical programs. However, independent of the representation, a Pos analysis can never come with any efficiency guarantees because of its potential exponential behaviour. This paper considers groundness analysis based on a simple subdomain of Pos and compares its precision with that of Pos.

A simple, syntactic algorithm for abstracting numeric constraints for groundness analysis is presented and proved correct. The technique uses neither projection nor temporary variables, and plugs a gap in the abstract interpretation literature.

Granularity control is a method to improve parallel execution performance by limiting excessive parallelism. The general idea is that if the gain obtained by executing a task in parallel is less than the overheads required to support parallel execution, then the task is better executed sequentially. Traditionally, in logic programming, task size is estimated from the sequential time-complexity of evaluating the task. Tasks are only executed in parallel if task size exceeds a pre-determined threshold. We argue in this paper that the estimation of complexity on its own is not an ideal metric for improving the performance of parallel programs through granularity control. We present a new metric for measuring granularity, based on a notion of distance. We present some initial results with two very simple methods of using this metric for granularity control. We then discuss how more sophisticated granularity control methods can be devised using the new metric.

One unique feature of logic languages is their ability to succinctly and declaratively express non-determinacy and hence search. Improving search efficiency is one of the main goals of AI and, by studying how redundant search may be factored out, this paper contributes to this goal. In logic programming, alternatives can be specified by a set of sentences defining the same predicate. By backtracking, considering in turn each of these sentences, these alternatives can be explored until a solution (if one exists) is found. However, though backtracking is essential for certain parts of a program, typically many predicates are deterministic, and most queries to a program have no more than one solution. Providing for non-determinacy can slow down the execution of a program on a uniprocessor and limit the scope for parallel execution on a multiprocessor. As a consequence, programmers are often forced to resort to the non-logical features of the language to ensure any determinacy is fully exploited. A number of papers on determinacy and its detection have been published. However, because of the diversity of applications for determinacy analysis, there has been a similar diversity of definitions of determinacy and its related concepts. This paper reformulates the determinacy definitions in a uniform way, identifying and contrasting the different approaches. Techniques for detecting and exploiting determinacy are also reviewed together with some directions for future research

Accurate variable sharing information is crucial both in the automatic parallelisation and in the optimisation of sequential logic programs. Analysis for variable sharing and term-dependence is thus an importance topic and many analyses have been proposed for inferring dependencies between the variables of a logic program. In this paper, a new approach to sharing analysis is described which infers sharing information to a much higher degree of accuracy than that of previous proposals. The analysis is founded on abstract substitutions which elegantly encode structural properties of substitutions. This enables the synergistic relationship between sharing and type information to be better exploited. The approach does not define a single analysis, as such, by in fact defines a framework for combining and refining existing analyses and deriving new analyses. Furthermore, in addition to defining new analyses, it simplifies the task of justifying an analysis. To illustrate, several new and powerful analyses are derived and proven safe in a way which is neat and concise. The usefulness of the analyses is demonstrated with examples.

Session subtyping answers the question of whether a program in a communicating system can be safely substituted for another, when their communication behaviours are described by session types. Asynchronous session subtyping is undecidable, hence the interest in devising sound, although incomplete, subtyping algorithms. State-of-the-art algorithms are formulated in terms of a data-structure called input trees. We show how input trees can be replaced by sets of traces, which opens up opportunities for applying techniques abstract interpretation techniques to the problem of asynchronous session subtyping. Sets of traces can be relaxed (enlarged) whilst still allowing subtyping to be observed, and one can choose relaxations that can be finitely represented, even when the input trees are arbitrarily large. We instantiate this strategy using regular expressions and show that it allows subtyping to be mechanically proven for communication patterns that were previously out of reach.

We address the satisfiability of systems of polynomial equations over bit-vectors. Instead of conventional bit-blasting, we exploit word-level inference to translate these systems into non-linear pseudo-boolean constraints. We derive the pseudo-booleans by simulating bit assignments through the addition of (linear) polynomials and applying a strong form of propagation by computing Gröbner bases. By handling bit assignments symbolically, the number of Gröbner basis calculations, along with the number of assignments, is reduced. The final Gröbner basis yields expressions for the bit-vectors in terms of the symbolic bits, together with non-linear pseudo-boolean constraints on the symbolic variables, modulo a power of two. The pseudo-booleans can be solved by translation into classical linear pseudo-boolean constraints (without a modulo) or by encoding them as propositional formulae, for which a novel translation process is described.

Much of an interpolation engine for bit-vector (BV) arithmetic can be constructed by observing that BV arithmetic can be modeled with linear integer arithmetic (LIA). Two BV formulae can thus be translated into two LIA formulae and then an interpolation engine for LIA used to derive an interpolant, albeit one expressed in LIA. The construction is completed by back-translating the LIA interpolant into a BV formula whose models coincide with those of the LIA interpolant. This paper develops a back-translation algorithm showing, for the first time, how back-translation can be universally applied, whatever the LIA interpolant. This avoids the need for deriving a BV interpolant by bit-blasting the BV formulae, as a backup process when back-translation fails. The new back-translation process relies on a novel geometric technique, called gapping, the correctness and practicality of which are demonstrated.

Octagons have enduring appeal because their domain operations are simple, readily mapping to for-loops which apply max, min and sum to the entries of a Difference Bound Matrix (DBM). In the quest for efficiency, arithmetic is often realised with double-precision floating-point, albeit at the cost of the certainty provided by arbitrary-precision rationals. In this paper we show how Compact DBMs (CoDBMs), which has recently been proposed as a memory refinement for DBMs, enable arithmetic calculation to be short-circuited in various domain operations. We also show how comparisons can be avoided by changing the tables which underpin CoDBMs. From the perspective of implementation, the optimisations are attractive because they too are conceptually simple, following the ethos of Octagons. Yet they halve the running time on rationals, putting CoDBMs on rationals on a par with DBMs on doubles.

The Octagon domain, which tracks a restricted class of two variable inequality, is the abstract domain of choice for many applications because its domain operations are either quadratic or cubic in the number of program variables. Octagon constraints are classically represented using a Difference Bound Matrix (DBM), where the entries in the DBM store bounds c for inequalities of the form x_i - x_j <= c, x_i + x_j <= c or -x_i - x_j <= c. The size of such a DBM is quadratic in the number of variables, giving a representation which can be excessively large for number systems such as rationals. This paper proposes a compact representation for DBMs, in which repeated numbers are factored out of the DBM. The paper explains how the entries of a DBM are distributed, and how this distribution can be exploited to save space and significantly speed-up long-running analyses. Moreover, unlike sparse representations, the domain operations retain their conceptually simplicity and ease of implementation whilst reducing memory usage.

This paper investigates the use of a Prolog coded SMT solver in tack- ling a well known constraints problem, namely packing a given set of consecutive squares into a given rectangle, and details the developments in the solver that this motivates. The packing problem has a natural model in the theory of quantifier-free integer difference logic, a theory supported by many SMT solvers. The solver used in this work exploits a data structure consisting of an incremental Floyd-Warshall matrix paired with a watch matrix that monitors the entailment status of integer difference constraints. It is shown how this structure can be used to build unsatisfiable theory cores on the y, which in turn allows theory learning to be incorporated into the solver. Further, it is shown that a problem-specific and non-standard approach to learning can be taken where symmetry breaking is incorporated into the learning stage, magnifying the e ect of learning. It is argued that the declarative framework allows the solver to be used in this white box manner and is a strength of the solver. The approach is experimentally evaluated.

The fact that Java is platform independent gives hackers the opportunity to write exploits that can target users on any platform, which has a JVM implementation. Metasploit is a well-known source of Java exploits and to circumvent detection by Anti Virus (AV) software, obfuscation techniques are routinely applied to make an exploit more difficult to recognise. Popular obfuscation techniques for Java include string obfuscation and applying reflection to hide method calls; two techniques that can either be used together or independently. This paper shows how to apply partial evaluation to remove these obfuscations and thereby improve AV matching. The paper presents a partial evaluator for Jimple, which is a typed three-address code suitable for optimisation and program analysis, and also demonstrates how the residual Jimple code, when transformed back into Java, improves the detection rates of a number of commercial AV products.

Although it is agreed that the Volgenant-Jonker (VJ) algorithm provides a fast way to approximate graph edit distance (GED), until now nobody has reported how the VJ algorithm can be tuned for this task. To this end, we revisit VJ and propose a series of refinements that improve both the speed and memory footprint without sacrificing accuracy in the GED approximation. We quantify the effectiveness of these optimisations by measuring distortion between control-flow graphs: a problem that arises in malware matching. We also document an unexpected behavioural property of VJ in which the time required to find shortest paths to unassigned nodes decreases as graph size increases, and explain how this phenomenon relates to the birthday paradox. Proceedings of 10th IAPR-TC-15 International Workshop, GbRPR 2015, Beijing, China, May 13-15, 2015.

The numerical domain of Octagons can be viewed as an exercise in simplicity: it trades expressiveness for efficiency and ease of implementation. The domain can represent unary and dyadic constraints where the coefficients are +1 or -1, so called octagonal constraints, and comes with operations that have cubic complexity. The central operation is closure which computes a canonical form by deriving all implied octagonal constraints from a given octagonal system. This paper investigates the role of incrementality, namely closing a system where only one constraint has been changed, which is a dominating use-case. We present two new incremental algorithms for closure both of which are conceptually simple and computationally efficient, and argue their correctness.

This paper revisits the semantics for Prolog with cut from the perspective of formulating a semantic base that is amenable to abstract interpretation. It argues that such a semantics should separate the question of divergence from questions pertaining to the number of answers and determinacy. It also shows how to replace prefix ordering, that is classically used in these semantics, with a domain that is setup for abstraction, whilst simultaneously retaining a fixpoint construction, albeit one in a stratified form.

As the volume of malware inexorably rises, comparison of binary code is of increasing importance to security analysts as a method of automatically classifying new malware samples; purportedly new examples of malware are frequently a simple evolution of existing code, whose differences stem only from a need to avoid detection. This paper presents a polynomial algorithm for calculating the differences between two binaries, obtained by fusing the well-known BinDiff algorithm with the Hungarian algorithm for bi-partite graph matching. This significantly improves the matching accuracy. Additionally a meaningful metric of similarity is calculated, based on graph edit distance, from which an informed comparison of the binaries can be made. The accuracy of this method over the standard approach is demonstrated.

Basing program analyses on formal semantics has a long and successful tradition in the logic programming paradigm. These analyses rely on results about the relative correctness of mathematically sophisticated semantics, and authors of such analyses often invest considerable effort into establishing these results. The development of interactive theorem provers such as Coq and their recent successes both in the field of program verification as well as in mathematics, poses the question whether these tools can be usefully deployed in logic programming. This paper presents formalisations in Coq of several general results about the correctness of semantics in different styles; forward and backward, top-down and bottom-up. The results chosen are paradigmatic of the kind of correctness theorems that semantic analyses rely on and are therefore well-suited to explore the possibilities afforded by the application of interactive theorem provers to this task, as well as the difficulties likely to be encountered in the endeavour. It turns out that the advantages offered by moving to a functional setting, including the possibility to apply higher-order abstract syntax, are considerable.

SAT Modulo Theories (SMT) is the problem of determining the satisfiability of a formula in which constraints, drawn from a given constraint theory T, are composed with logical connectives. The DPLL(T) approach to SMT has risen to prominence as a technique for solving these quantifier-free problems. The key idea in DPLL(T) is to closely couple unit propagation in the propositional part of the problem with theory propagation in the constraint component. In this paper it is demonstrated how reification provides a natural way for orchestrating this in the setting of logic programming. This allows an elegant implementation of DPLL(T) solvers in Prolog. The work is motivated by a problem in reverse engineering, that of type recovery from binaries. The solution to this problem requires an SMT solver where the theory is that of rational-tree constraints, a theory not supported in off-the-shelf SMT solvers, but realised as unification in many Prolog systems. The solver is benchmarked against a number of type recovery problems, and compared against a lazy-basic SMT solver built on PicoSAT.

Loop leaping is the colloquial name given to a form of program analysis in which summaries are derived for nested loops starting from the innermost loop and proceeding in a bottom-up fashion considering one more loop at a time. Loop leaping contrasts with classical approaches to finding loop invariants that are iterative; loop leaping is compositional requiring each stratum in the nest of loops to be considered exactly once. The approach is attractive in predicate abstraction where disjunctive domains are increasingly used that present long ascending chains. This paper proposes a simple and an efficient approach for loop leaping for these domains based on viewing loops as closure operators.

The abstract domain of polyhedra lies at the heart of many program analysis techniques. However, its operations can be expensive, precluding their application to polyhedra that involve many variables. This paper describes a new approach to computing polyhedral domain operations. The core of this approach is an algorithm to calculate variable elimination (projection) based on parametric linear programming. The algorithm enumerates only non-redundant inequalities of the projection space, hence permits anytime approximation of the output.

The question of what constraints must hold for a predicate to behave as a (partial) function, is key to understanding the behaviour of a logic program. It has been shown how this question can be answered by combining backward analysis, a form of analysis that propagates determinacy requirements against the control flow, with a component for deriving so-called mutual exclusion conditions. The latter infers conditions sufficient to ensure that if one clause yields an answer then another cannot. This paper addresses the challenge of how to compute these conditions by showing that this problem can be reformulated as that of vertex enumeration. Whilst directly applicable in logic programming, the method might well also find application in reasoning about type classes.

This paper presents an elegant algorithm for existential quantifier elimination using incremental SAT solving. This approach contrasts with existing techniques in that it is based solely on manipulating the SAT instance rather than requiring any reengineering of the SAT solver or needing an auxiliary data-structure such as a BDD. The algorithm combines model enumeration with the generation of shortest prime implicants so as to converge onto a quantifier-free formula presented in CNF. We apply the technique to a number of hardware circuits and transfer functions to demonstrate the effectiveness of the method.

This paper describes an approximate quantifier elimination procedure for propositional Boolean formulae. The method is based on computing prime implicants using SAT and successively refining over-approximations of a given formula. This construction naturally leads to an anytime algorithm, that is, it can be interrupted at anytime without compromising soundness. This contrasts with classical monolithic (all or nothing) approaches based on resolution or model enumeration.

Recently it has been shown how transfer functions for linear template constraints can be derived for bit-vector programs by operating over propositional Boolean formulae. The drawback of this method is that it relies on existential quantifier elimination, which induces a computational bottleneck. The contribution of this paper is a novel method for synthesising transfer functions that does not rely on quantifier elimination. We demonstrate the practicality of the method for generating transfer functions for both intervals and octagons.

Traditionally, transfer functions have been manually designed for each operation in a program. Recently, however, there has been growing interest in computing transfer functions, motivated by the desire to reason about sequences of operations that constitute basic blocks. This paper focuses on deriving transfer functions for intervals --- possibly the most widely used numeric domain --- and shows how they can be computed from Boolean formulae which are derived through bit-blasting. This approach is entirely automatic, avoids complicated elimination algorithms, and provides a systematic way of handling wrap-arounds (integer overflows and underflows) which arise in machine arithmetic.

A succinct SAT solver is presented that exploits the control provided by delay declarations to implement watched literals and unit propagation. Despite its brevity the solver is surprisingly powerful and its elegant use of Prolog constructs is presented as a programming pearl.

One approach to verifying bit-twiddling algorithms is to derive invariants between the bits that constitute the variables of a program. Such invariants can often be described with systems of congruences where in each equation $\vec{c} \cdot \vec{x} = d \mod m$, (unknown variable m)$ is a power of two, $\vec{c}$ is a vector of integer coefficients, and $\vec{x}$ is a vector of propositional variables (bits). Because of the low-level nature of these invariants and the large number of bits that are involved, it is important that the transfer functions can be derived automatically. We address this problem, showing how an analysis for bit-level congruence relationships can be decoupled into two parts: (1) a SAT-based abstraction (compilation) step which can be automated, and (2) an interpretation step that requires no SAT-solving. We exploit triangular matrix forms to derive transfer functions efficiently, even in the presence of large numbers of bits. Finally we propose program transformations that improve the analysis results.

Verifying the correctness of microcontroller programs in presence of bitwise instructions, loops, and indirect data access poses difficult challenges. In particular, it is necessary to show that an indirect write does not mutate registers, which are indirectly addressable. To prove this property, among others, this paper presents a relational binary-code semantics and details how this can be used to compute program invariants in terms of bit-level congruences. Moreover, it demonstrates how congruences can be combined with intervals to derive accurate ranges, as well as information about strided indirect memory accesses.

Weakly relational numeric domains express restricted classes of linear inequalities that strike a balance between what can be described and what can be efficiently computed. Popular weakly relational domains such as bounded differences and octagons have found application in model checking and abstract interpretation. This paper introduces logahedra, which are more expressiveness than octagons, but less expressive than arbitrary systems of two variable per inequality constraints. Logahedra allow coefficients of inequalities to be powers of two whilst retaining many of the desirable algorithmic properties of octagons.

Polyhedra are widely used in model checking and abstract interpretation. Polyhedral analysis is effective when the relationships between variables are linear, but suffers from imprecision when it is necessary to take into account the integrality of the represented space. Imprecision also arises when non-linear constraints occur. Moreover, in terms of tractability, even a space defined by linear constraints can become unmanageable owing to the excessive number of inequalities. Thus it is useful to identify those inequalities whose omission has least impact on the represented space. This paper shows how these issues can be addressed in a novel way by growing the integer hull of the space and approximating the number of integral points within a bounded polyhedron.

This paper proposes a new approach for deriving invariants that are systems of congruence equations where the modulo is a power of 2. The technique is an amalgam of SAT-solving, where a propositional formula is used to encode the semantics of a basic block, and abstraction, where the solutions to the formula are systematically combined and summarised as a system of congruence equations. The resulting technique is more precise than existing congruence analyses since a single optimal transfer function is derived for a basic block as a whole.

Variables in programs are usually confined to a fixed number of bits and results that require more bits are truncated. Due to the use of 32-bit and 64-bit variables, inadvertent overflows are rare. However, a sound static analysis must reason about overflowing calculations and conversions between unsigned and signed integers; the latter remaining a common source of subtle programming errors. Rather than polluting an analysis with the low-level details of modelling two's complement wrapping behaviour, this paper presents a computationally light-weight solution based on polyhedral analysis which eliminates the need to check for wrapping when evaluating most (particularly linear) assignments.

The abstract domain of polyhedra is sufficiently expressive to be deployed in verification. One consequence of the richness of this domain is that long, possibly infinite, sequences of polyhedra can arise in the analysis of loops. Widening and narrowing have been proposed to infer a single polyhedron that summarises such a sequence of polyhedra. Motivated by precision losses encountered in verification, we explain how the classic widening/narrowing approach can be refined by an improved extrapolation strategy. The insight is to record inequalities that are thus far found to be unsatisfiable in the analysis of a loop. These so-called landmarks hint at the amount of widening necessary to reach stability. This extrapolation strategy, which refines widening with thresholds, can infer post-fixpoints that are precise enough not to require narrowing. Unlike previous techniques, our approach interacts well with other domains, is fully automatic, conceptually simple and precise on complex loops.

Detecting symmetries is crucial to logic synthesis, technology mapping, detecting function equivalence under unknown input correspondence, and ROBDD minimization. State-of-the-art is represented by Mishchenko's algorithm. In this paper we present an efficient anytime algorithm for detecting symmetries in Boolean functions represented as ROBDDs, that output pairs of symmetric variables until a prescribed time bound is exceeded. The algorithm is complete in that given sufficient time it is guaranteed to find all symmetric pairs. The complexity of this algorithm is in O(n^4+n|G|+|G|^3) where n is the number of variables and |G| the number of nodes in the ROBDD, and it is thus competitive with Mishchenko's |G|^3 algorithm in the worst-case since n << |G|. However, our algorithm performs significantly better because the anytime approach only requires lightweight data structure support and it offers unique opportunities for optimization.

In program development it is useful to know that a call to a Prolog program will not inadvertently leave a choice-point on the stack. Determinacy inference has been proposed for solving this problem yet the analysis was found to be wanting in that it could not infer determinacy conditions for programs that contained cuts or applied certain tests to select a clause. This paper shows how to remedy these serious deficiencies. It also addresses the problem of identifying those predicates which can be rewritten in a more deterministic fashion. To this end, a radically new form of determinacy inference is introduced, which is founded on ideas in ccp, that is capable of reasoning about the way bindings imposed by a rightmost goal can make a leftmost goal deterministic.

A description in the Jacobs and Langen domain is a set of sharing groups where each sharing group is a set of program variables. The presence of a sharing group in a description indicates that all the variables in the group can be bound to terms that contain a common variable. The expressiveness of the domain, alas, is compromised by its intractability. Not only are descriptions potentially exponential in size, but abstract unification is formulated in terms of an operation, called closure under union, that is also exponential. This paper shows how abstract unification can be reformulated so that closures can be collapsed in two senses. Firstly, one closure operation can be folded into another so as to reduce the total number of closures that need to be computed. Secondly, the remaining closures can be applied to smaller descriptions. Therefore, although the operation remains exponential, the overhead of closure calculation is reduced. Experimental evaluation suggests that the cost of analysis can be substantially reduced by collapsing closures.

Sharing analysis is widely deployed in the optimisation, specialisation and parallelisation of logic programs. Each abstract unification operation over the classic Jacobs and Langen domain involves the calculation of a closure operation that has exponential worst-case complexity. This paper explores a new tactic for improving performance: laziness. The idea is to compute partial sharing information eagerly and recover full sharing information lazily. The net result is an analysis that runs in a fraction of the time of the classic analysis and yet has comparable precision.

Despite the ubiquity of ROBDDs in program analysis, and extensive literature on ROBDD minimisation, there is a dearth of work on approximating ROBDDs. The need for approximation arises because many ROBDD operations result in an ROBDD whose size is quadratic in the size of the inputs. Furthermore, if ROBDDs are used in abstract interpretation, the running time of the analysis is related not only to the complexity of the individual ROBDD operations but also the number of operations applied. The number of operations is, in turn, constrained by the number of times a Boolean function can be weakened before stability is achieved. This paper proposes a widening that can be used to both constrain the size of an ROBDD and also ensure that the number of times that it is weakened is bounded by some given constant. The widening can be used to either systematically approximate from above (i.e. derive a weaker function) or below (i.e. infer a stronger function).

The intrinsic cost of polyhedra has lead to research on more tractable sub-classes of linear inequalities. Rather than committing to the precision of such a sub-class, this paper presents a projection algorithm that works directly on any sparse system of inequalities and which sacrifices precision only when necessary. The algorithm is based on a novel combination of the Fourier-Motzkin algorithm (for exact projection) and Simplex (for approximate projection). By reformulating the convex hull operation in terms of projection, conversion to the frame representation is avoided altogether. Experimental results conducted on logic programs demonstrate that the resulting analysis is efficient and precise.

This paper presents a determinacy inference analysis for logic programs. The analysis infers determinacy conditions that, if satisfied by a call, ensures that it computes at most one answer and that answer is generated only once. The principal component of the technique is a goal-independent analysis of individual clauses. This derives a condition for a call that ensures only one clause in the matching predicate possesses a successful derivation. Another key component of the analysis is backwards reasoning stage that strengthens these conditions to derive properties on a call that assure determinacy. The analysis has applications in program development, implementation and specialisation.

One recent advance in program development has been the application of abstract interpretation to verify the partial correctness of a (constraint) logic program. Traditionally forwards analysis has been applied that starts with an initial goal and traces the execution in the direction of the control-flow to approximate the program state at each program point. This is often enough to verify assertions that a property holds. The dual approach is to apply backwards analysis to propagate properties of the allowable states against the control-flow to infer queries for which the program will not violate any assertion. Backwards analysis also underpins other program development tasks such as verifying the termination of a logic program or proving that a logic program with a delay mechanism cannot reduce to a state that contains sub-goals which suspend indefinitely. This paper reviews various backwards analyses that have been proposed for logic programs, identifying common threads in these techniques. The analyses are explained through a series of worked examples. The paper concludes with some suggestions for research in backwards analysis for logic program development.

Reasoning about termination is a key issue in logic program development. One classic technique for proving termination is to construct a well-founded order on goals that decreases between successive goals in a derivation. In practise, this is achieved with the aid of a level mapping that maps atoms to natural numbers. This paper examines why it can be difficult to base termination proofs on natural level mappings that directly relate to the recursive structure of the program. The notions of bounded-recurrency and bounded-acceptability are introduced to alleviate these problems. These concepts are equivalent to the classic notions of recurrency and acceptability respectively, yet provide practical criteria for constructing termination proofs in terms of natural level mappings for definite logic programs. Moreover, the construction is entirely modular in that termination conditions are derived in a bottom-up fashion by considering, in turn, each the strongly connected components of the program.

This paper presents a backward sharing analysis for logic programs. The analysis computes pre-conditions for a query that guarantee a given post-condition is satisfied after the query is successfully executed. The analysis uses a pair sharing domain and is capable of inferring pre-conditions that ensure the absence of sharing. This, in turn, has many applications in logic programming. The work is unique in that it demonstrates that backward analysis is applicable even for properties that are not closed under instantiation.

One recent development in logic programming has been the application of abstract interpretation to verify the partial correctness of a logic program with respect to a given set of assertions. One approach to verification is to apply forward analysis that starts with an initial goal and traces the execution in the direction of the control-flow to approximate the program state at each program point. This is often enough to verify that the assertions hold. The dual approach is to apply backward analysis to propagate properties of the allowable states against the control-flow to infer queries for which the program will not violate any assertion. This paper is a systematic comparison of these two approaches to verification. The paper reports some equivalence results that relate the relative power of various forward and backward analysis frameworks.

A goal-independent suspension analysis is presented that infers a class of goals for which a logic program with delays can be executed without suspension. The crucial point is that the analysis does not verify that an (abstract) goal does not lead to suspension but rather it infers (abstract) goals which do not lead to suspension.

This paper presents a backward type analysis for logic programs. Given type signatures for a collection of selected predicates such as builtin or library predicates, the analysis infers type signatures for other predicates such that the execution of any query satisfying the inferred type signatures will not violate the type signatures for the selected predicates. Thus, the backward type analysis generalises type checking in which the programmer manually specifies type signatures for all predicates that are checked for consistency by a type checker.

A buffer overrun occurs in a C program when input is read into a buffer whose length exceeds that of the buffer. Overruns often lead to crashes and are a widespread form of security vulnerability. This paper describes an analysis for detecting overruns before deployment which is conservative in the sense that it locates every possible buffer overrun. The paper details the subtle relationship between overrun analysis and pointer analysis and explains how buffers can be modeled with a linear number of variables. As far as we know, the paper gives the first formal account of how this software and security problem can be tackled with abstract interpretation, setting it on a firm, mathematical basis.

This paper explores the spatial domain of sets of inequalities where each inequality contains at most two variables - a domain that is richer than intervals and more tractable than general polyhedra. We present a complete suite of efficient domain operations for linear systems with two variables per inequality with unrestricted coefficients. We exploit a tactic in which a system of inequalities with at most two variables per inequality is decomposed into a series of projections - one for each two dimensional plane. The decomposition enables all domain operations required for abstract interpretation to be expressed in terms of the two dimensional case. The resulting operations are efficient and include a novel planar convex hull algorithm. Empirical evidence suggests that widening can be applied effectively, ensuring tractability.

Boolean functions are ubiquitous in the analysis of (constraint) logic programs. The domain of positive Boolean functions, Pos, has been used for expressing, for example, groundness, finiteness and sharing dependencies. The performance of an analyser based on Boolean functions is critically dependent on the way in which the functions are represented. This paper discusses multiheaded clauses as a representation of positive Boolean functions. The domain operations for multiheaded clauses are conceptually simple and can be implemented straightforwardly in Prolog. Moreover these operations generalise those for the less algorithmically complex operations of propositional Horn clauses, leading to naturally stratified algorithms. The multiheaded clause representation is used to build a Pos-based groundness analyser. The analyser performs surprisingly well and scales smoothly, not requiring widening to analyse any program in the benchmark suite.

Abstract interpretation theory has successfully been used for constructing algorithms to statically determine run-time properties of programs. Central is the notion of an abstract domain, describing certain properties of interest about the program. In logic programming, program analyses typically fall into two different categories: either they detect program points where the property definitely holds (universal analyses) or possibly holds (existential analyses). We study the relation between such analyses in the case where the concrete domain is a lattice join-generated by its set of join-irreducible elements. Although our intended application is for logic programming, the theory is sufficiently general for possible applications to other languages.

The domain of definite Boolean functions, $\mydef$, can be used to express the groundness of, and trace grounding dependencies between, program variables in (constraint) logic programs. In this paper, previously unexploited computational properties of $\mydef$ are utilised to develop an efficient and succinct groundness analyser that can be coded in Prolog. In particular, entailment checking is used to prevent unnecessary least upper bound calculations. It is also demonstrated that join can be defined in terms of other operations, thereby eliminating code and removing the need for preprocessing formulae to a normal form. This saves space and time. Furthermore, the join can be adapted to straightforwardly implement the downward closure operator that arises in set sharing analyses. Experimental results indicate that the new $\mydef$ implementation gives favourable results in comparison with BDD-based groundness analyses.

A procedure is described for tightening domain constraints of finite domain logic programs by applying a static analysis based on convex polyhedra. Individual finite domain constraints are over-approximated by polyhedra to describe the solution space over n integer variables as an n dimensional polyhedron. This polyhedron is then approximated, using projection, as an n dimensional bounding box that can be used to specialise and improve the domain constraints. The analysis can be implemented straightforwardly and an empirical evaluation of the specialisation technique is given.

Precise mode information is important for compiler optimisations and in program development tools. Within the framework of abstract compilation, the precision of a mode analysis depends, in part, on the expressiveness of the abstract domain and its associated abstraction function. This paper considers abstract domains for polymorphically typed logic programs and shows how specialised domains may be constructed for each type in the program. These domains capture the degree of instantiation to a high level of precision. By providing a generic definition of abstract unification, the abstraction of a program using these domains is formalised. The domain construction procedure is fully implemented using the Godel language and tested on a number of example programs to demonstrate the viability of the approach.

Def, the domain of definite Boolean functions, expresses (sure) dependencies between the program variables of, say, a constraint program. Share, on the other hand, captures the (possible) variable sharing between the variables of a logic program. The connection between these domains has been explored in the domain comparison and decomposition literature. We develop this link further and show how the meet (as well as the join) of Def can be modeled with efficient (quadratic) operations on Share. Further, we show how by compressing and widening Share and by rescheduling meet operations, we can construct a dependency analysis that is surprisingly fast and precise, and comes with time- and space- performance guarantees. Unlike some other approaches, our analysis can be coded straightforwardly in Prolog.

Granularity control is a method to improve parallel execution performance by limiting excessive parallelism. The general idea is that if the gain obtained by executing a task in parallel is less than the overheads required to support parallel execution, then the task is better executed sequentially. Traditionally, in logic programming, task size is estimated as the sequential time-complexity of evaluating the task. Tasks are only executed in parallel if task size exceeds a pre-determined threshold. We argue in this paper that the estimation of task complexity, on its own, is not an ideal metric for improving the performance of parallel programs through granularity control. We present a new metric for measuring granularity, based on a notion of emphdistance. We present some initial results with two very simple methods of using this metric for granularity control. We then discuss how more sophisticated granularity control methods can be devised using the new metric.

This paper focusses on practical analysis for logic programs with delay. The method described is for downward-closed program properties and, in particular, groundness. A program transformation is defined which eliminates the delay statements but still enables an accurate approximation of the behaviour of delayed goals to be traced by the analyser. An implementation has been built which shows that the analysis can be both accurate and efficient.

We show how termination of logic programs with delay declarations can be proven. Three features are distinctive of this work: (a) we assume that predicates can be used in several modes; (b) we show that block declarations, which are a very simple delay construct, are sufficient; (c) we take the selection rule into account, assuming it to be as in most Prolog implementations. Our method is based on identifying the so-called robust predicates, for which the textual position of an atom using this predicate is irrelevant. The method can be used to verify existing programs, and to assist in writing new programs. As a byproduct, we also show how programs can be proven to be free from occur-check and floundering.

We present verification methods for logic programs with delay declarations, showing how type and instantiation errors related to built-ins can be avoided, and how termination can be ensured. Three features are distinctive of this work: (a) we assume that predicates can be used in several modes; (b) we show that block declarations, which are a particularly simple delay construct, are sufficient to ensure the desired properties; (c) we take the selection rule into account, assuming it to be the rule of most Prolog implementations. These methods can be used both to verify existing programs and to assist in writing new programs.

The paper proposes a technique for inferring conditions on goals that, when satisfied, ensure that a goal is sufficiently coarse-grained to warrant parallel evaluation. The method is powerful enough to reason about divide-and-conquer programs, and in the case of quicksort, for instance, can infer that a quicksort goal has a time complexity that exceeds 64 resolution steps (a threshold for spawning) if the input list is of length 10 or more. This gives a simple run-time tactic for controlling spawning. The method has been proved correct, can be implemented straightforwardly, has been demonstrated to be useful on a parallel machine, and, in contrast with much of the previous work on time-complexity analysis of logic programs, does not require any complicated difference equation solving machinery.

The objective of control generation in logic programming is to automatically derive a computation rule for a program that is efficient and yet does not compromise program correctness. Progress in solving this important problem has been slow and, to date, only partial solutions have been proposed where the generated programs are either incorrect or inefficient. We show how the control generation problem can be tackled with a simple automatic transformation that relies on information about the depths of derivations. To prove correctness of our transform we introduce the notion of a semi delay recurrent program which generalises previous ideas in the termination literature for reasoning about logic programs with dynamic selection rules.

Argument size relationships are useful in termination analysis which, in turn, is important in program synthesis and goal-replacement transformations. We show how a precise analysis for inter-argument size relationships, formulated in terms of abstract interpretation, can be implemented straightforwardly in a language with constraint support like CLP(R) or SICStus version 3. The analysis is based on polyhedral approximations and uses a simple relaxation technique to calculate least upper bounds and a delay method to improve the precision of widening. To the best of our knowledge, and despite its simplicity, the analysis derives relationships to an accuracy that is either comparable or better than any existing technique.

As typed logic programming becomes more mainstream, system building tools like partial deduction systems will need to be mapped from untyped languages to typed ones. It is important, however, when mapping techniques across that the new techniques should exploit the type system as much as possible. in this paper, we show how norms which play a crucial role in termination analysis, can be generated from the prescribed types of a logic program. Interestingly, the types highlight restrictions of earlier norms and suggest how these norms can be extended to obtain some very general and powerful notions of norm which can be used to measure any term in an almost arbitrary way. We see our work on norm derivation as a contribution to the termination analysis of typed logic programs which, in particular, forms an essential part of offline partial deduction systems.

A new and powerful approach to threading is proposed, that is designed to improve the responsiveness of concurrent logic programs for distributed, real-time AI applications. The technique builds on previously proposed scheduling techniques to improve responsiveness by synchronously passing control and data directly from a producer to a consumer. Furthermore, synchronous transfer of data requires less buffering and so less garbage is produced. Arguments are also passed in registers, further reducing overheads.

Accurate variable sharing information is crucial both in the automatic parallelisation and in the optimisation of sequential logic programs. Analysis for possible variable sharing is thus an important topic in logic programming and many analyses have been proposed for inferring dependencies between the variables of a program, for instance, by combining domains and analyses. This paper develops the combined domain theme by explaining how term structure, and in particular linearity, can be represented in a sharing group format. This enables aliasing behaviour to be more precisely captured; groundness information to be more accurately propagated; and in addition, refines the tracking and application of linearity. In practical terms, this permits aliasing and groundness to be inferred to a higher degree of accuracy than in previous proposals and also can speed up the analysis itself. Correctness is formally proven.

Analyses for variable sharing and freeness are important both in the automatic parallelisation and in the optimisation of sequential logic programs. In this paper, a new analysis is described which can infer sharing and freeness information to an unusually high degree of accuracy. By encoding structural properties of substitutions in a sharing group fashion, a powerful depth-k sharing and freeness analysis is synthesised which exploits the synergy between tracing sharing information and tracking term structure. The analysis propagates groundness with the accuracy of sharing groups and yet can precisely infer sharing and freeness. Correctness is formally proven.

A compilation technique is proposed for concurrent logic programs called schedule analysis. Schedule analysis deduces at compile-time a partial schedule for the processes of a program by partitioning the atoms of each clause into threads. Threads are totally ordered sets of atoms whose relative ordering is determined by a scheduler. Threads reduce scheduler activity and permit a wealth of traditional Prolog optimisations to be applied to the program. A framework for schedule analysis is proposed and this defines a procedure for creating threads. A safety result is presented stating the conditions under which the work of the scheduler can be reduced from ordering processes to ordering threads. Schedule analysis has been integrated into a compiler and implementation has suggested that it can play a central role in compilation. Optimisations which follow from schedule analysis include a reduction in scheduling, the removal of synchronisation checks, the simplification of unification, decreased garbage collection and a reduction in argument copying.

Serialisation analysis reduces the time a concurrent logic program spends communicating and scheduling. It fits granularity analysis and schedule analysis into a single unified framework for partitioning a program into grains for parallel evaluation and ordering grains for sequential evaluation. Serialisation analysis is simple, avoids the complexity of thresholding, and unlike previous proposals for controlling granularity, is based on threads. The threads avoid the creation of suspensions and therefore reduce scheduler activity. Threads also act as indivisible units of work, and therefore inhibit the parallel evaluation of fine-grained processes. Furthermore, serialisation analysis incurs no extra run-time overhead.

Ordering optimisations are optimisations that can be applied to a concurrent logic program when the atoms of a clause are known to be ordered. In this paper ordering optimisations are reviewed, reformulated and refined. The paper explains how ordering optimisations can be realised in terms of abstract interpretation and shows that by, building on schedule analysis, simple, efficient and accurate forms of abstract interpretation can achieved. The paper outlines how to: identify instances of unification which can be simplified or removed; distinguish repeated synchronisation instructions; indicate which redundant checks can be removed when producers are ordered before consumers in the same thread; identify which variables can be accessed without dereferencing; indicate where variable initialisation and unification can be simplified; and show which variables can be allocated to an environment. Some safety checks can also be removed by using mode information.

COTS components are ubiquitous in military, industrial and governmental systems. However, the bene?fits of reduced development and maintainance costs are compromised by security concerns. Since source code is unavailable, security audits necessarily occur at the binary level. Push-button formal method techniques, such as model checking and abstract interpretation, can support this process by, among other things, inferring ranges of values for registers. Ranges aid the security engineer in checking for vulnerabilities that relate, for example, to integer wrapping, uninitialised variables and bu?er over ows. Yet the lack of structure in binaries limits the e?ffectiveness of classical range analyses based on widening. This paper thus contributes a simple but novel range analysis, formulated in terms of linear programming, which calculates ranges without manual intervention.

Strictness analysis is crucial for the efficient implementation of the lazy functional languages. A related technique for the concurrent logic languages (CLLs) called schedule analysis is presented which divides at compile-time a CLL program into threads of totally ordered atoms, whose relative ordering is determined at run-time. The technique enables the enqueuing and dequeuing of processes to be reduced, synchronisation tests to be partially removed, introduces the possibility of using unboxed arguments, and permits variables to be migrated from a heap to a stack to affect a form of compile-time garbage collection. The implementation is outlined and some preliminary results are given.

Loop leaping is the colloquial name given to a form of program analysis in which summaries are derived for nested loops starting from the innermost loop and proceeding in a bottom-up fashion considering one more loop at a time. Loop leaping contrasts with classical approaches to finding loop invariants that are iterative; loop leaping is compositional requiring each stratum in the nest of loops to be considered exactly once. The approach is attractive in predicate abstraction where disjunctive domains are increasingly used that present long ascending chains. This paper proposes a simple and an efficient approach for loop leaping for these domains based on viewing loops as closure operators.

Reconstructing the meaning of a program from its binary executable is known as reverse engineering; it has a wide range of applications in software security, exposing piracy, legacy systems, etc. Since reversing is ultimately a search for meaning, there is much interest in inferring a type (a meaning) for the elements of a binary in a consistent way. Unfortunately existing approaches do not guarantee any semantic relevance for their reconstructed types. This paper presents a new and semantically-founded approach that provides strong guarantees for the reconstructed types. Key to our approach is the derivation of a witness program in a high-level language alongside the reconstructed types. This witness has the same semantics as the binary, is type correct by construction, and it induces a (justifiable) type assignment on the binary. Moreover, the approach effectively yields a type-directed decompiler. We formalise and implement the approach for reversing Minx, an abstraction of x86, to MinC, a type-safe dialect of C with recursive datatypes. Our evaluation compiles a range of textbook C algorithms to MinX and then recovers the original structures.

The question of what constraints must hold for a predicate to behave as a (partial) function, is key to understanding the behaviour of a logic program. It has been shown how this question can be answered by combining backward analysis, a form of analysis that propagates determinacy requirements against the control flow, with a component for deriving so-called mutual exclusion conditions. The latter infers conditions sufficient to ensure that if one clause yields an answer then another cannot. This paper addresses the challenge of how to compute these conditions by showing that this problem can be reformulated as that of vertex enumeration. Whilst directly applicable in logic programming, the method might well also find application in reasoning about type classes.

Proofs of the mathematical foundations and propositions and theorems stated and used in our paper in the TPLP Special Issue on ICLP 2011.

Logic programming is sometimes described as relational programming: a paradigm in which the programmer specifies and composes n-ary relations using systems of constraints. An advanced logic programming environment will provide tools that abstract these relations to transform, optimise, or even verify the correctness of a logic program. This talk will show that these concepts, namely relations, constraints and abstractions, turn out to also be important in the reverse engineer process that underpins the discovery of bugs within the security industry.

Benchmark files and evaluation of the type-directed decompiler described in the paper "From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes"

Proceedings for the Thirteenth International Symposium on Functional and Logic Programming, FLOPS 2016, held in Kochi, Japan, March 4-6, 2016.

Proof appendix to accompany the paper, "From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes"

Proofs of the mathematical foundations and propositions and theorems stated and used in our paper in the TPLP Special Issue on ICLP 2011.

This note provides proof of some new decompositional results for generalized symmetries in ROBDDs. These results permit generalized symmetries to be found with algorithms that are formulated as a series of passes one for each variable in the ROBDD, which is the basis of the anytime approach to symmetry detection.

A description in the Jacobs and Langen domain is a set of sharing groups where each sharing group is a set of program variables. The presence of a sharing group in a description indicates that all the variables in the group can be bound to terms that contain a common variable. The expressiveness of the domain, alas, is compromised by its intractability. Not only are descriptions potentially exponential in size, but abstract unification is formulated in terms of an operation, called closure under union, that is also exponential. This paper shows how abstract unification can be reformulated so that closures can be collapsed in two senses. Firstly, one closure operation can be folded into another so as to reduce the total number of closures that need to be computed. Secondly, the remaining closures can be applied to smaller descriptions. Therefore, although the operation remains exponential, the overhead of closure calculation is reduced. Experimental evaluation suggests that the cost of analysis can be substantially reduced by collapsing closures.

This note provides proof of some new implicational relationships between generalized symmetries. These relationships are formulated in terms of twelve symmetry types. Six of these symmetries are denoted T_n^x_i,x_j where the index n?[1,6] indicates that a specific co-factor equivalence property holds between the variables x_i and x_j. The other six symmetries are denoted neg T_n^x_i,x_j, and indicate that one co-factor is equivalent to the negation of the other. The relationships that are specified take the form, if T_p^x_i,x_j and T_q^x_j,x_k hold then T_r^x_i,x_j holds where T_p,T_q and T_r denote one of these twelve symmetry types.

One recent development in logic programming has been the application of abstract interpretation to verify the partial correctness of a logic program with respect to a given set of assertions. One approach to verification is to apply forward analysis that starts with an initial goal and traces the execution in the direction of the control-flow to approximate the program state at each program point. This is often enough to verify that the assertions hold. The dual approach is apply backward analysis to propagate properties of the allowable states against the control-flow to infer queries for which the program will not violate any assertion. This paper is a systematic comparison of these two approaches to verification. The paper reports some equivalence results that relate the relative power of various forward and backward analysis frameworks.

Zaffanella presents an intriguing abstract unification algorithm for tracing set-sharing with linearity and freeness as part of this doctoral thesis. This note provides a short correctness proof for the main novel aspect of this algorithm.

One recurring problem in program development is that of understanding how to re-use code developed by a third party. In the context of (constraint) logic programming, part of this problem reduces to figuring out how to query a program. If the logic program does not come with any documentation, then the programmer is forced to either experiment with queries in an textitad hoc fashion or trace the control-flow of the program (backward) to infer the modes in which a predicate must be called so as to avoid an instantiation error. This paper presents an abstract interpretation scheme that automates the latter technique. The analysis presented in this paper can infer moding properties which if satisfied by the initial query, come with the guarantee that the program and query can never generate any moding or instantiation errors. Other applications of the analysis are discussed. The paper explains how abstract domains with certain computational properties (they condense) can be used to trace control-flow backward (right-to-left) to infer useful properties of initial queries. A correctness argument is presented and an implementation is reported.

Boolean functions are often represented as binary decision diagrams (BDDs). BDDs are potentially of exponential size in the number of variables of the function. Boolean functions drawn from Pos (the class of positive Boolean functions) and Def (the class of definite Boolean functions) are often used to describe the groundness of, and grounding dependencies between, program variables in (constraint) logic programs. mypos-based analyses are often implemented using BDDs which are sometimes problematically large. Since the complexities of the most frequently used domain operations are quadratic in the size of the input BDDs, widening BDDs for space is also a widening for time, hence is important for scalability. Two algorithms for widening BDDs for space are presented and are discussed (with relation to groundness analysis).

This note clarifies how to handle solution gathering meta-calls, asserts and retracts in the groundness analysis of Prolog.

This paper formalises an analysis of finite domain programs and the resultant program transformation. The analysis adds low valency (domain) constraints to clauses in order to reduce search. The technique is outlined with a worked example and then formalised using abstract interpretation. Correctness of the analysis and of the transformation is proved.

Polyhedral cones can be represented by sets of linear inequalities that express inter-variable relationships. These inequalities express inter-variable relationships that are quantified by the ratios between the variable coefficients. However, linear inequalities over a non-negative variable domain with only unit variable coefficients and no constants other than zero can represent relationships that can be valid in non-numeric domains. For instance, if variables are either non-negative or zero itself, that is, a strictly two-point domain, then 0 <= x, 0 <= y, x <= y, expresses a dependency between x and y, since if y is known to be zero, then so is x. By defining an abstraction operator that effectively puts aside the scaling coefficients whilst retaining the inter-variable aspect of these relationships polyhedral cones can express the same dependency information as Def, a class of Boolean function. Boolean functions are considered over a fixed finite set of variables and Def is a subset of the positive Boolean functions, which return the value true when every variable returns true. Def is a complete lattice ordered by logical consequence and it will be shown that the abstract cones also form a complete lattice, ordered by set inclusion, that is isomorphic to Def.

Soft deadlines are significant in systems in which a bound on the response time is important, but the failure to meet the response time is not a disaster. Soft deadlines occur, for example, in telephony and switching networks. We investigate how to put probabilistic bounds on the time-complexity of a concurrent logic program by combining (on-line) profiling with an (off-line) probabilistic complexity analysis. The profiling collects information on the likelihood of case selection and the analysis uses this information to infer the probability of an agent terminating within k steps. Although the approach does not reason about synchronization, we believe that its simplicity and good (essentially quadratic) complexity mean that it is a promising first step in reasoning about soft deadlines.

Analyses for sharing and freeness are important in the optimisation and parallelisation of logic programs. By using suitable abstract analogs for concrete operations like renaming, restriction, unification and extension sharing and freeness analysis can be constructed from a standard fixed-point framework. Extension is required in the clause exit mechanisms and is typically formulated in terms of restriction and matching. Matching also arises as goal-head unification in normalised programs in which the (formal) arguments of each clause head are distinct variables. Abstract matching, however, is rarely given special attention and is usually implemented by abstract unification. This paper remedies this, contributing a series of useful, practical and formally-justified abstract matching algorithms for the popular domains Share, Share x Free and Share x Free x Lin The matching algorithms are both useful and important because they can outperform their corresponding unification algorithms in both speed and precision.

Analyses for possible variable sharing and definite freeness are important both in the automatic parallelisation and in the optimisation of sequential logic programs. In this paper, a new efficient approach to analysis is described which can infer sharing and freeness information to an unusually high degree of accuracy. The analysis exploits a confluence property of the unification algorithm to split the analysis into two distinct phases. The two phase analysis improves efficiency by enabling each phase of the analysis to manipulate relatively simple data-structures. The precision follows from the combination of domains. The analysis propagates groundness with the accuracy of sharing groups and yet infers sharing and freeness to a precision which exceeds that of a normal freeness analysis. High precision compoundness information can be derived too. The usefulness of the analysis is demonstrated with worked examples. Correctness is formally proven.