-
Regular Path Clauses and Their Application in Solving Loops
Authors:
Bishoksan Kafle,
John P. Gallagher,
Manuel V. Hermenegildo,
Maximiliano Klemen,
Pedro López-García,
José F. Morales
Abstract:
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 between the values of variables, or program properties such as cost, on successive loop iterations. Recurrence solvers are capable of computing closed forms for some recurrences, thus deriving precise relationships capt…
▽ More
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 between the values of variables, or program properties such as cost, on successive loop iterations. Recurrence solvers are capable of computing closed forms for some recurrences, thus deriving precise relationships capturing the complete loop execution. However, many recurrences extracted from loops cannot be solved, due to their having multiple recursive cases or multiple arguments. In the literature, several techniques for approximating the solution of unsolvable recurrences have been proposed. The approach presented in this paper is to define transformations based on regular path expressions and loop counters that (i) transform multi-path loops to single-path loops, giving rise to recurrences with a single recursive case, and (ii) transform multi-argument recurrences to single-argument recurrences, thus enabling the use of recurrence solvers on the transformed recurrences. Using this approach, precise solutions can sometimes be obtained that are not obtained by approximation methods.
△ Less
Submitted 9 September, 2021;
originally announced September 2021.
-
Analysis and Transformation of Constrained Horn Clauses for Program Verification
Authors:
Emanuele De Angelis,
Fabio Fioravanti,
John P. Gallagher,
Manuel V. Hermenegildo,
Alberto Pettorossi,
Maurizio Proietti
Abstract:
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 software systems. We present specialisation-based techniques for translating verification problems for different programming languages, and in general software systems, into satisfiability problems for constrained Horn claus…
▽ More
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 software systems. We present specialisation-based techniques for translating verification problems for different programming languages, and in general software systems, into satisfiability problems for constrained Horn clauses (CHCs), a term that has become popular in the verification field to refer to CLP programs. Then, we describe static analysis techniques for CHCs that may be used for inferring relevant program properties, such as loop invariants. We also give an overview of some transformation techniques based on specialisation and fold/unfold rules, which are useful for improving the effectiveness of CHC satisfiability tools. Finally, we discuss future developments in applying these techniques.
△ Less
Submitted 2 August, 2021;
originally announced August 2021.
-
An Experiment Combining Specialization with Abstract Interpretation
Authors:
John P. Gallagher,
Robert Glück
Abstract:
It was previously shown that control-flow refinement can be achieved by a program specializer incorporating property-based abstraction, to improve termination and complexity analysis tools. We now show that this purpose-built specializer can be reconstructed in a more modular way, and that the previous results can be achieved using an off-the-shelf partial evaluation tool, applied to an abstract i…
▽ More
It was previously shown that control-flow refinement can be achieved by a program specializer incorporating property-based abstraction, to improve termination and complexity analysis tools. We now show that this purpose-built specializer can be reconstructed in a more modular way, and that the previous results can be achieved using an off-the-shelf partial evaluation tool, applied to an abstract interpreter. The key feature of the abstract interpreter is the abstract domain, which is the product of the property-based abstract domain with the concrete domain. This language-independent framework provides a practical approach to implementing a variety of powerful specializers, and contributes to a stream of research on using interpreters and specialization to achieve program transformations.
△ Less
Submitted 6 August, 2020;
originally announced August 2020.
-
From Big-Step to Small-Step Semantics and Back with Interpreter Specialisation
Authors:
John P. Gallagher,
Manuel Hermenegildo,
Bishoksan Kafle,
Maximiliano Klemen,
Pedro López García,
José Morales
Abstract:
We investigate representations of imperative programs as constrained Horn clauses. Starting from operational semantics transition rules, we proceed by writing interpreters as constrained Horn clause programs directly encoding the rules. We then specialise an interpreter with respect to a given source program to achieve a compilation of the source language to Horn clauses (an instance of the first…
▽ More
We investigate representations of imperative programs as constrained Horn clauses. Starting from operational semantics transition rules, we proceed by writing interpreters as constrained Horn clause programs directly encoding the rules. We then specialise an interpreter with respect to a given source program to achieve a compilation of the source language to Horn clauses (an instance of the first Futamura projection). The process is described in detail for an interpreter for a subset of C, directly encoding the rules of big-step operational semantics for C. A similar translation based on small-step semantics could be carried out, but we show an approach to obtaining a small-step representation using a linear interpreter for big-step Horn clauses. This interpreter is again specialised to achieve the translation from big-step to small-step style. The linear small-step program can be transformed back to a big-step non-linear program using a third interpreter. A regular path expression is computed for the linear program using Tarjan's algorithm, and this regular expression then guides an interpreter to compute a program path. The transformation is realised by specialisation of the path interpreter. In all of the transformation phases, we use an established partial evaluator and exploit standard logic program transformation to remove redundant data structures and arguments in predicates and rename predicates to make clear their link to statements in the original source program.
△ Less
Submitted 6 August, 2020;
originally announced August 2020.
-
Polyvariant Program Specialisation with Property-based Abstraction
Authors:
John P. Gallagher
Abstract:
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 specialisation in a standard online specialisation algorithm. Specialisation is a program transformation that transforms a program with respect to given constraints that restrict its behaviour. Polyvariant specialisation…
▽ More
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 specialisation in a standard online specialisation algorithm. Specialisation is a program transformation that transforms a program with respect to given constraints that restrict its behaviour. Polyvariant specialisation refers to the generation of two or more specialised versions of the same program code. The same program point can be reached more than once during a computation, with different constraints applying in each case, and polyvariant specialisation allows different specialisations to be realised. A property-based abstraction uses a finite set of properties to define a finite set of abstract versions of predicates, ensuring that only a finite number of specialised versions is generated. The particular choice of properties is critical for polyvariance; too few versions can result in insufficient specialisation, while too many can result in an increase of code size with no corresponding efficiency gains. Using examples, we show the flexibility of specialisation with property-based abstraction and discuss its application in control flow refinement, verification, termination analysis and dimension-based specialisation.
△ Less
Submitted 20 August, 2019;
originally announced August 2019.
-
Towards a General Framework for Static Cost Analysis of Parallel Logic Programs
Authors:
Maximiliano Klemen,
Pedro Lopez-Garcia,
John P. Gallagher,
Jose F. Morales,
Manuel V. Hermenegildo
Abstract:
The estimation and control of resource usage is now an important challenge in an increasing number of computing systems. In particular, requirements on timing and energy arise in a wide variety of applications such as internet of things, cloud computing, health, transportation, and robots. At the same time, parallel computing, with (heterogeneous) multi-core platforms in particular, has become the…
▽ More
The estimation and control of resource usage is now an important challenge in an increasing number of computing systems. In particular, requirements on timing and energy arise in a wide variety of applications such as internet of things, cloud computing, health, transportation, and robots. At the same time, parallel computing, with (heterogeneous) multi-core platforms in particular, has become the dominant paradigm in computer architecture. Predicting resource usage on such platforms poses a difficult challenge. Most work on static resource analysis has focused on sequential programs, and relatively little progress has been made on the analysis of parallel programs, or more specifically on parallel logic programs. We propose a novel, general, and flexible framework for setting up cost equations/relations which can be instantiated for performing resource usage analysis of parallel logic programs for a wide range of resources, platforms and execution models. The analysis estimates both lower and upper bounds on the resource usage of a parallel program (without executing it) as functions on input data sizes. In addition, it also infers other meaningful information to better exploit and assess the potential and actual parallelism of a system. We develop a method for solving cost relations involving the max function that arise in the analysis of parallel programs. Finally, we instantiate our general framework for the analysis of logic programs with Independent And-Parallelism, report on an implementation within the CiaoPP system, and provide some experimental results. To our knowledge, this is the first approach to the cost analysis of parallel logic programs.
△ Less
Submitted 30 July, 2019;
originally announced July 2019.
-
Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis
Authors:
Jesús J. Doménech,
John P. Gallagher,
Samir Genaim
Abstract:
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 precision. Several techniques have been suggested for different programming models, typically tailored to improving precision for a particular analysis. In this paper we explore the use of partial evaluation of Horn clauses as…
▽ More
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 precision. Several techniques have been suggested for different programming models, typically tailored to improving precision for a particular analysis. In this paper we explore the use of partial evaluation of Horn clauses as a general-purpose technique for control-flow refinement for integer transitions systems. These are control-flow graphs where edges are annotated with linear constraints describing transitions between corresponding nodes, and they are used in many program analysis tools. Using partial evaluation for control-flow refinement has the clear advantage over other approaches in that soundness follows from the general properties of partial evaluation; in particular, properties such as termination and complexity are preserved. We use a partial evaluation algorithm incorporating property-based abstraction, and show how the right choice of properties allows us to prove termination and to infer complexity of challenging programs that cannot be handled by state-of-the-art tools. We report on the integration of the technique in a termination analyzer, and its use as a preprocessing step for several cost analyzers. Under consideration for acceptance in TPLP.
△ Less
Submitted 31 July, 2019; v1 submitted 29 July, 2019;
originally announced July 2019.
-
Detecting and Diagnosing Energy Issues for Mobile Applications
Authors:
Xueliang Li,
Yuming Yang,
Yepang liu,
John P. Gallagher,
Kaishun Wu
Abstract:
Energy efficiency is an important criterion to judge the quality of mobile apps, but one third of our randomly sampled apps suffer from energy issues that can quickly drain battery power. To understand these issues, we conducted an empirical study on 27 well-maintained apps such as Chrome and Firefox, whose issue tracking systems are publicly accessible. Our study revealed that the main root cause…
▽ More
Energy efficiency is an important criterion to judge the quality of mobile apps, but one third of our randomly sampled apps suffer from energy issues that can quickly drain battery power. To understand these issues, we conducted an empirical study on 27 well-maintained apps such as Chrome and Firefox, whose issue tracking systems are publicly accessible. Our study revealed that the main root causes of energy issues include unnecessary workload and excessively frequent operations. Surprisingly, these issues are beyond the application of present technology on energy issue detection. We also found that 20.6% of energy issues can only manifest themselves under specific contexts such as poor network performance, but such contexts are again neglected by present technology. Therefore, we proposed a novel testing framework for detecting energy issues in real-world apps. Our framework examines apps with well-designed input sequences and runtime contexts. To identify the root causes mentioned above, we employed a machine learning algorithm to cluster the workloads and further evaluate their necessity. For the issues concealed by the specific contexts, we carefully set up several execution contexts to pinpoint them. More importantly, we developed leading edge technology, e.g. pre-designing input sequences with potential energy overuse and tuning tests on-the-fly, to achieve high efficacy in detecting energy issues. A large-scale evaluation shows that 91.6% issues detected in our test were previously unknown to developers. On average, these issues double the energy costs of the apps. Furthermore, our test achieves a low number of false positives. Finally, we show how our test reports can help developers fix the issues.
△ Less
Submitted 22 March, 2019; v1 submitted 4 January, 2019;
originally announced January 2019.
-
An iterative approach to precondition inference using constrained Horn clauses
Authors:
Bishoksan Kafle,
John P. Gallagher,
Graeme Gange,
Peter Schachte,
Harald Sondergaard,
Peter J. Stuckey
Abstract:
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 (CHCs) are used to model the program and assertions in a uniform way, and we use standard abstract interpretations to derive an over-approximation of the set of unsafe initial states. The precondition then i…
▽ More
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 (CHCs) are used to model the program and assertions in a uniform way, and we use standard abstract interpretations to derive an over-approximation of the set of unsafe initial states. The precondition then is the constraint corresponding to the complement of that set, under-approximating the set of safe initial states. This idea of complementation is not new, but previous attempts to exploit it have suffered from the loss of precision. Here we develop an iterative specialisation algorithm to give more precise, and in some cases optimal safety conditions. The algorithm combines existing transformations, namely constraint specialisation, partial evaluation and a trace elimination transformation. The last two of these transformations perform polyvariant specialisation, leading to disjunctive constraints which improve precision. The algorithm is implemented and tested on a benchmark suite of programs from the literature in precondition inference and software verification competitions.
△ Less
Submitted 16 April, 2018;
originally announced April 2018.
-
Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation
Authors:
John P. Gallagher,
Rob van Glabbeek,
Wendelin Serwe
Abstract:
This volume contains the joint proceedings of MARS 2018, the third workshop on Models for Formal Analysis of Real Systems, and VPT 2018, the sixth international workshop on Verification and Program Transformation, held together on April 20, 2018 in Thessaloniki, Greece, as part of ETAPS 2018, the European Joint Conferences on Theory and Practice of Software.
MARS emphasises modelling over verifi…
▽ More
This volume contains the joint proceedings of MARS 2018, the third workshop on Models for Formal Analysis of Real Systems, and VPT 2018, the sixth international workshop on Verification and Program Transformation, held together on April 20, 2018 in Thessaloniki, Greece, as part of ETAPS 2018, the European Joint Conferences on Theory and Practice of Software.
MARS emphasises modelling over verification. It aims at discussing the lessons learned from making formal methods for the verification and analysis of realistic systems. Examples are:
(1) Which formalism is chosen, and why?
(2) Which abstractions have to be made and why?
(3) How are important characteristics of the system modelled?
(4) Were there any complications while modelling the system?
(5) Which measures were taken to guarantee the accuracy of the model?
We invited papers that present full models of real systems, which may lay the basis for future comparison and analysis. An aim of the workshop is to present different modelling approaches and discuss pros and cons for each of them. Alternative formal descriptions of the systems presented at this workshop are encouraged, which should foster the development of improved specification formalisms.
VPT aims to provide a forum where people from the areas of program transformation and program verification can fruitfully exchange ideas and gain a deeper understanding of the interactions between those two fields. These interactions have been beneficial in both directions. On the one hand, methods and tools developed in the field of program transformation, such as partial deduction, partial evaluation, fold/unfold transformations, and supercompilation, are applied with success to verification, in particular to the verification of infinite state and parameterized systems. On the other hand, methods developed in program verification, such as model checking, abstract interpretation, SAT and SMT solving, and automated theorem proving, are used to enhance program transformation techniques, thereby making these techniques more powerful and useful in practice.
△ Less
Submitted 23 March, 2018;
originally announced March 2018.
-
Tree dimension in verification of constrained Horn clauses
Authors:
Bishoksan Kafle,
John P. Gallagher,
Pierre Ganty
Abstract:
In this paper, we show how the notion of tree dimension can be used in the verification of constrained Horn clauses (CHCs). The dimension of a tree is a numerical measure of its branching complexity and the concept here applies to Horn clause derivation trees. Derivation trees of dimension zero correspond to derivations using linear CHCs, while trees of higher dimension arise from derivations usin…
▽ More
In this paper, we show how the notion of tree dimension can be used in the verification of constrained Horn clauses (CHCs). The dimension of a tree is a numerical measure of its branching complexity and the concept here applies to Horn clause derivation trees. Derivation trees of dimension zero correspond to derivations using linear CHCs, while trees of higher dimension arise from derivations using non-linear CHCs. We show how to instrument CHCs predicates with an extra argument for the dimension, allowing a CHC verifier to reason about bounds on the dimension of derivations. Given a set of CHCs $P$, we define a transformation of $P$ yielding a dimension bounded set of CHCs $P^{\leq{k}}$. The set of derivations for $P^{\leq{k}}$ consists of the derivations for $P$ that have dimension at most $k$. We also show how to construct a set of clauses denoted $P^{>{k}}$ whose derivations have dimension exceeding $k$. We then present algorithms using these constructions to decompose a CHC verification problem. One variation of this decomposition considers derivations of successively increasing dimension. The paper includes descriptions of implementations and experimental results. Under consideration for publication in Theory and Practice of Logic Programming (TPLP).
△ Less
Submitted 6 March, 2018; v1 submitted 4 March, 2018;
originally announced March 2018.
-
Pre-proceedings of the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017)
Authors:
Fabio Fioravanti,
John P. Gallagher
Abstract:
This volume constitutes the pre-proceedings of the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), held on 10-12th October 2017 in Namur, Belgium, and co-located with the 19th International Symposium on Principles and Practice of Declarative Programming (PPDP 2017). After discussion at the symposium papers will go through a second round of refereeing…
▽ More
This volume constitutes the pre-proceedings of the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), held on 10-12th October 2017 in Namur, Belgium, and co-located with the 19th International Symposium on Principles and Practice of Declarative Programming (PPDP 2017). After discussion at the symposium papers will go through a second round of refereeing and selection for the formal proceedings.
△ Less
Submitted 31 August, 2017; v1 submitted 24 August, 2017;
originally announced August 2017.
-
A Source-level Energy Optimization Framework for Mobile Applications
Authors:
Xueliang Li,
John P. Gallagher
Abstract:
Energy efficiency can have a significant influence on user experience of mobile devices such as smartphones and tablets. Although energy is consumed by hardware, software optimization plays an important role in saving energy, and thus software developers have to participate in the optimization process. The source code is the interface between the developer and hardware resources. In this paper, we…
▽ More
Energy efficiency can have a significant influence on user experience of mobile devices such as smartphones and tablets. Although energy is consumed by hardware, software optimization plays an important role in saving energy, and thus software developers have to participate in the optimization process. The source code is the interface between the developer and hardware resources. In this paper, we propose an energy-optimization framework guided by a source code energy model that allows developers to be aware of energy usage induced by the code and to apply very targeted source-level refactoring strategies. The framework also lays a foundation for the code optimization by automatic tools. To the best of our knowledge, our work is the first that achieves this for a high-level language such as Java. In a case study, the experimental evaluation shows that our approach is able to save from 6.4% to 50.2% of the CPU energy consumption in various application scenarios.
△ Less
Submitted 18 August, 2016;
originally announced August 2016.
-
Solving non-linear Horn clauses using a linear Horn clause solver
Authors:
Bishoksan Kafle,
John P. Gallagher,
Pierre Ganty
Abstract:
In this paper we show that checking satisfiability of a set of non-linear Horn clauses (also called a non-linear Horn clause program) can be achieved using a solver for linear Horn clauses. We achieve this by interleaving a program transformation with a satisfiability checker for linear Horn clauses (also called a solver for linear Horn clauses). The program transformation is based on the notion o…
▽ More
In this paper we show that checking satisfiability of a set of non-linear Horn clauses (also called a non-linear Horn clause program) can be achieved using a solver for linear Horn clauses. We achieve this by interleaving a program transformation with a satisfiability checker for linear Horn clauses (also called a solver for linear Horn clauses). The program transformation is based on the notion of tree dimension, which we apply to a set of non-linear clauses, yielding a set whose derivation trees have bounded dimension. Such a set of clauses can be linearised. The main algorithm then proceeds by applying the linearisation transformation and solver for linear Horn clauses to a sequence of sets of clauses with successively increasing dimension bound. The approach is then further developed by using a solution of clauses of lower dimension to (partially) linearise clauses of higher dimension. We constructed a prototype implementation of this approach and performed some experiments on a set of verification problems, which shows some promise.
△ Less
Submitted 15 July, 2016;
originally announced July 2016.
-
Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis
Authors:
John P. Gallagher,
Philipp Rümmer
Abstract:
This volume contains the proceedings of HCVS 2016, the Third Workshop on Horn Clauses for Verification and Synthesis which was held on April 3, 2016 in Eindhoven, The Netherlands as a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2016). Many program verification and synthesis problems of interest can be modeled directly using Horn clauses and many rece…
▽ More
This volume contains the proceedings of HCVS 2016, the Third Workshop on Horn Clauses for Verification and Synthesis which was held on April 3, 2016 in Eindhoven, The Netherlands as a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2016). Many program verification and synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the CLP and CAV communities have centered around efficiently solving problems presented as Horn clauses. The Third Workshop on Horn Clauses for Verification and Synthesis was organised with the aim to bring together researchers working in the two communities of Constraint/Logic Programming and Program Verification on the topic of Horn clause based analysis, verification and synthesis. Horn clauses for verification and synthesis have been advocated by these two communities in different times and from different perspectives, and this workshop is organized to stimulate interaction and a fruitful exchange and integration of experiences.
△ Less
Submitted 14 July, 2016;
originally announced July 2016.
-
ENTRA: Whole-Systems Energy Transparency
Authors:
Kerstin Eder,
John P. Gallagher,
Pedro Lopez-Garcia,
Henk Muller,
Zorana Bankovic,
Kyriakos Georgiou,
Remy Haemmerle,
Manuel V. Hermenegildo,
Bishoksan Kafle,
Steve Kerrison,
Maja Kirkeby,
Maximiliano Klemen,
Xueliang Li,
Umer Liqat,
Jeremy Morse,
Morten Rhiger,
Mads Rosendahl
Abstract:
Promoting energy efficiency to a first class system design goal is an important research challenge. Although more energy-efficient hardware can be designed, it is software that controls the hardware; for a given system the potential for energy savings is likely to be much greater at the higher levels of abstraction in the system stack. Thus the greatest savings are expected from energy-aware softw…
▽ More
Promoting energy efficiency to a first class system design goal is an important research challenge. Although more energy-efficient hardware can be designed, it is software that controls the hardware; for a given system the potential for energy savings is likely to be much greater at the higher levels of abstraction in the system stack. Thus the greatest savings are expected from energy-aware software development, which is the vision of the EU ENTRA project. This article presents the concept of energy transparency as a foundation for energy-aware software development. We show how energy modelling of hardware is combined with static analysis to allow the programmer to understand the energy consumption of a program without executing it, thus enabling exploration of the design space taking energy into consideration. The paper concludes by summarising the current and future challenges identified in the ENTRA project.
△ Less
Submitted 18 June, 2016; v1 submitted 13 June, 2016;
originally announced June 2016.
-
An Energy-Aware Programming Approach for Mobile Application Development Guided by a Fine-Grained Energy Model
Authors:
Xueliang Li,
John P. Gallagher
Abstract:
Energy efficiency has a significant influence on user experience of battery-driven devices such as smartphones and tablets. It is shown that software optimization plays an important role in reducing energy consumption of system. However, in mobile devices, the conventional nature of compiler considers not only energy-efficiency but also limited memory usage and real-time response to user inputs, w…
▽ More
Energy efficiency has a significant influence on user experience of battery-driven devices such as smartphones and tablets. It is shown that software optimization plays an important role in reducing energy consumption of system. However, in mobile devices, the conventional nature of compiler considers not only energy-efficiency but also limited memory usage and real-time response to user inputs, which largely limits the compiler's positive impact on energy-saving. As a result, the code optimization relies more on developers. In this paper, we propose an energy-aware programming approach, which is guided by an operation-based source-code-level energy model. And this approach is placed at the end of software engineering life cycle to avoid distracting developers from guaranteeing the correctness of system. The experimental result shows that our approach is able to save from 6.4% to 50.2% of the overall energy consumption depending on different scenarios.
△ Less
Submitted 17 May, 2016;
originally announced May 2016.
-
Interpolant Tree Automata and their Application in Horn Clause Verification
Authors:
Bishoksan Kafle,
John P. Gallagher
Abstract:
This paper investigates the combination of abstract interpretation over the domain of convex polyhedra with interpolant tree automata, in an abstraction-refinement scheme for Horn clause verification. These techniques have been previously applied separately, but are combined in a new way in this paper. The role of an interpolant tree automaton is to provide a generalisation of a spurious counterex…
▽ More
This paper investigates the combination of abstract interpretation over the domain of convex polyhedra with interpolant tree automata, in an abstraction-refinement scheme for Horn clause verification. These techniques have been previously applied separately, but are combined in a new way in this paper. The role of an interpolant tree automaton is to provide a generalisation of a spurious counterexample during refinement, capturing a possibly infinite set of spurious counterexample traces. In our approach these traces are then eliminated using a transformation of the Horn clauses. We compare this approach with two other methods; one of them uses interpolant tree automata in an algorithm for trace abstraction and refinement, while the other uses abstract interpretation over the domain of convex polyhedra without the generalisation step. Evaluation of the results of experiments on a number of Horn clause verification problems indicates that the combination of interpolant tree automaton with abstract interpretation gives some increase in the power of the verification tool, while sometimes incurring a performance overhead.
△ Less
Submitted 10 July, 2016; v1 submitted 25 January, 2016;
originally announced January 2016.
-
Decomposition by tree dimension in Horn clause verification
Authors:
Bishoksan Kafle,
John P. Gallagher,
Pierre Ganty
Abstract:
In this paper we investigate the use of the concept of tree dimension in Horn clause analysis and verification. The dimension of a tree is a measure of its non-linearity - for example a list of any length has dimension zero while a complete binary tree has dimension equal to its height. We apply this concept to trees corresponding to Horn clause derivations. A given set of Horn clauses P can be tr…
▽ More
In this paper we investigate the use of the concept of tree dimension in Horn clause analysis and verification. The dimension of a tree is a measure of its non-linearity - for example a list of any length has dimension zero while a complete binary tree has dimension equal to its height. We apply this concept to trees corresponding to Horn clause derivations. A given set of Horn clauses P can be transformed into a new set of clauses P=<k, whose derivation trees are the subset of P's derivation trees with dimension at most k. Similarly, a set of clauses P>k can be obtained from P whose derivation trees have dimension at least k + 1. In order to prove some property of all derivations of P, we systematically apply these transformations, for various values of k, to decompose the proof into separate proofs for P=<k and P>k (which could be executed in parallel). We show some preliminary results indicating that decomposition by tree dimension is a potentially useful proof technique. We also investigate the use of existing automatic proof tools to prove some interesting properties about dimension(s) of feasible derivation trees of a given program.
△ Less
Submitted 11 December, 2015;
originally announced December 2015.
-
Optimised determinisation and completion of finite tree automata
Authors:
John P. Gallagher,
Mai Ajspur,
Bishoksan Kafle
Abstract:
Determinisation and completion of finite tree automata are important operations with applications in program analysis and verification. However, the complexity of the classical procedures for determinisation and completion is high. They are not practical procedures for manipulating tree automata beyond very small ones. In this paper we develop an algorithm for determinisation and completion of fin…
▽ More
Determinisation and completion of finite tree automata are important operations with applications in program analysis and verification. However, the complexity of the classical procedures for determinisation and completion is high. They are not practical procedures for manipulating tree automata beyond very small ones. In this paper we develop an algorithm for determinisation and completion of finite tree automata, whose worst-case complexity remains unchanged, but which performs far better than existing algorithms in practice. The critical aspect of the algorithm is that the transitions of the determinised (and possibly completed) automaton are generated in a potentially very compact form called product form, which can reduce the size of the representation dramatically. Furthermore, the representation can often be used directly when manipulating the determinised automaton. The paper contains an experimental evaluation of the algorithm on a large set of tree automata examples.
△ Less
Submitted 1 November, 2017; v1 submitted 11 November, 2015;
originally announced November 2015.
-
Inferring Parametric Energy Consumption Functions at Different Software Levels: ISA vs. LLVM IR
Authors:
Umer Liqat,
Kyriakos Georgiou,
Steve Kerrison,
Pedro Lopez-Garcia,
John P. Gallagher,
Manuel V. Hermenegildo,
Kerstin Eder
Abstract:
The static estimation of the energy consumed by program executions is an important challenge, which has applications in program optimization and verification, and is instrumental in energy-aware software development. Our objective is to estimate such energy consumption in the form of functions on the input data sizes of programs. We have developed a tool for experimentation with static analysis wh…
▽ More
The static estimation of the energy consumed by program executions is an important challenge, which has applications in program optimization and verification, and is instrumental in energy-aware software development. Our objective is to estimate such energy consumption in the form of functions on the input data sizes of programs. We have developed a tool for experimentation with static analysis which infers such energy functions at two levels, the instruction set architecture (ISA) and the intermediate code (LLVM IR) levels, and reflects it upwards to the higher source code level. This required the development of a translation from LLVM IR to an intermediate representation and its integration with existing components, a translation from ISA to the same representation, a resource analyzer, an ISA-level energy model, and a map** from this model to LLVM IR. The approach has been applied to programs written in the XC language running on XCore architectures, but is general enough to be applied to other languages. Experimental results show that our LLVM IR level analysis is reasonably accurate (less than 6.4% average error vs. hardware measurements) and more powerful than analysis at the ISA level. This paper provides insights into the trade-off of precision versus analyzability at these levels.
△ Less
Submitted 4 November, 2015;
originally announced November 2015.
-
Fine-Grained Energy Modeling for the Source Code of a Mobile Application
Authors:
Xueliang Li,
John P. Gallagher
Abstract:
Energy efficiency has a significant influence on user experience of battery-driven devices such as smartphones and tablets. The goal of an energy model for source code is to lay a foundation for the application of energy-saving techniques during software development. The challenge is to relate hardware energy consumption to high-level application code, considering the complex run-time context and…
▽ More
Energy efficiency has a significant influence on user experience of battery-driven devices such as smartphones and tablets. The goal of an energy model for source code is to lay a foundation for the application of energy-saving techniques during software development. The challenge is to relate hardware energy consumption to high-level application code, considering the complex run-time context and software stack. Traditional techniques build the energy model by map** a hardware energy model onto software constructs; this approach faces obstacles when the software stack consists of a number of abstract layers. Another approach that has been followed is to utilize hardware or operating system features to estimate software energy information at a coarse level of granularity such as blocks, methods or even applications. In this paper, we explain how to construct a fine-grained energy model for the source code, which is based on "energy operations" identified directly from the source code and able to provide more valuable information for code optimization. We apply the approach to a class of applications based on a game-engine, and explain the wider applicability of the method.
△ Less
Submitted 18 May, 2016; v1 submitted 14 October, 2015;
originally announced October 2015.
-
Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification
Authors:
Bishoksan Kafle,
John P. Gallagher
Abstract:
We present an approach to constrained Horn clause (CHC) verification combining three techniques: abstract interpretation over a domain of convex polyhedra, specialisation of the constraints in CHCs using abstract interpretation of query-answer transformed clauses, and refinement by splitting predicates. The purpose of the work is to investigate how analysis and transformation tools developed for c…
▽ More
We present an approach to constrained Horn clause (CHC) verification combining three techniques: abstract interpretation over a domain of convex polyhedra, specialisation of the constraints in CHCs using abstract interpretation of query-answer transformed clauses, and refinement by splitting predicates. The purpose of the work is to investigate how analysis and transformation tools developed for constraint logic programs (CLP) can be applied to the Horn clause verification problem. Abstract interpretation over convex polyhedra is capable of deriving sophisticated invariants and when used in conjunction with specialisation for propagating constraints it can frequently solve challenging verification problems. This is a contribution in itself, but refinement is needed when it fails, and the question of how to refine convex polyhedral analyses has not been studied much. We present a refinement technique based on interpolants derived from a counterexample trace; these are used to drive a property-based specialisation that splits predicates, leading in turn to more precise convex polyhedral analyses. The process of specialisation, analysis and splitting can be repeated, in a manner similar to the CEGAR and iterative specialisation approaches.
△ Less
Submitted 2 December, 2014;
originally announced December 2014.
-
Analysis and Transformation Tools for Constrained Horn Clause Verification
Authors:
John P. Gallagher,
Bishoksan Kafle
Abstract:
Several techniques and tools have been developed for verification of properties expressed as Horn clauses with constraints over a background theory (CHC). Current CHC verification tools implement intricate algorithms and are often limited to certain subclasses of CHC problems. Our aim in this work is to investigate the use of a combination of off-the-shelf techniques from the literature in analysi…
▽ More
Several techniques and tools have been developed for verification of properties expressed as Horn clauses with constraints over a background theory (CHC). Current CHC verification tools implement intricate algorithms and are often limited to certain subclasses of CHC problems. Our aim in this work is to investigate the use of a combination of off-the-shelf techniques from the literature in analysis and transformation of Constraint Logic Programs (CLPs) to solve challenging CHC verification problems. We find that many problems can be solved using a combination of tools based on well-known techniques from abstract interpretation, semantics-preserving transformations, program specialisation and query-answer transformations. This gives insights into the design of automatic, more general CHC verification tools based on a library of components.
△ Less
Submitted 15 May, 2014;
originally announced May 2014.
