-
Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation
Authors:
Geoffrey W. Hamilton,
Temesghen Kahsai,
Maurizio Proietti
Abstract:
These proceedings include selected papers presented at the 9th Workshop on Horn Clauses for Verification and Synthesis and the Tenth International Workshop on Verification and Program Transformation, both affiliated with ETAPS 2022.
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…
▽ More
These proceedings include selected papers presented at the 9th Workshop on Horn Clauses for Verification and Synthesis and the Tenth International Workshop on Verification and Program Transformation, both affiliated with ETAPS 2022.
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 HCVS series of workshops aims to bring together researchers working in the communities of Constraint/Logic Programming (e.g., ICLP and CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g., CADE, IJCAR), on the topic of Horn clause based analysis, verification, and synthesis.
Horn clauses for verification and synthesis have been advocated by these communities in different times and from different perspectives and HCVS is organized to stimulate interaction and a fruitful exchange and integration of experiences.
The aim of the VPT workshop is to bring together researchers working in the fields of Program Verification and Program Transformation.
There is a great potential for beneficial interactions between these two fields because:
1) On one hand, methods and tools developed in the field of Program Transformation such as partial evaluation, fold/unfold transformations, and supercompilation, have all been applied with success for the verification of infinite state and parameterized systems.
2) On the other hand, model checking, abstract interpretation, SAT and SMT solving and automated theorem proving have been used to enhance program transformation techniques. Moreover, the formal certification of program transformation tools, such as automated refactoring tools and compilers, has recently attracted considerable interest, posed major challenges.
△ Less
Submitted 19 November, 2022;
originally announced November 2022.
-
The Ethics of Biosurveillance
Authors:
S. K. Devitt,
P. W. J. Baxter,
G. Hamilton
Abstract:
Governments must keep agricultural systems free of pests that threaten agricultural production and international trade. Biosecurity surveillance already makes use of a wide range of technologies, such as insect traps and lures, geographic information systems, and diagnostic biochemical tests. The rise of cheap and usable surveillance technologies such as remotely piloted aircraft systems (RPAS) pr…
▽ More
Governments must keep agricultural systems free of pests that threaten agricultural production and international trade. Biosecurity surveillance already makes use of a wide range of technologies, such as insect traps and lures, geographic information systems, and diagnostic biochemical tests. The rise of cheap and usable surveillance technologies such as remotely piloted aircraft systems (RPAS) presents value conflicts not addressed in international biosurveillance guidelines. The costs of keeping agriculture pest-free include privacy violations and reduced autonomy for farmers. We argue that physical and digital privacy in the age of ubiquitous aerial and ground surveillance is a natural right to allow people to function freely on their land. Surveillance methods must be co-created and justified through using ethically defensible processes such as discourse theory, value-centred design and responsible innovation to forge a cooperative social contract between diverse stakeholders. We propose an ethical framework for biosurveillance activities that balances the collective benefits for food security with individual privacy: (1) establish the boundaries of a biosurveillance social contract; (2) justify surveillance operations for the farmers, researchers, industry, the public and regulators; (3) give decision makers a reasonable measure of control over their personal and agricultural data; and (4) choose surveillance methodologies that give the appropriate information. The benefits of incorporating an ethical framework for responsible biosurveillance innovation include increased participation and accumulated trust over time. Long term trust and cooperation will support food security, producing higher quality data overall and mitigating against anticipated information gaps that may emerge due to disrespecting landholder rights
△ Less
Submitted 23 November, 2021;
originally announced November 2021.
-
The Next 700 Program Transformers
Authors:
Geoffrey Hamilton
Abstract:
In this paper, we describe a hierarchy of program transformers in which the transformer at each level of the hierarchy builds on top of those at lower levels. The program transformer at level 1 of the hierarchy corresponds to positive supercompilation, and that at level 2 corresponds to distillation. We prove that the transformers at each level terminate. We then consider the speedups that can be…
▽ More
In this paper, we describe a hierarchy of program transformers in which the transformer at each level of the hierarchy builds on top of those at lower levels. The program transformer at level 1 of the hierarchy corresponds to positive supercompilation, and that at level 2 corresponds to distillation. We prove that the transformers at each level terminate. We then consider the speedups that can be obtained at each level in the hierarchy, and try to characterise the improvements that can be made.
△ Less
Submitted 27 August, 2021; v1 submitted 25 August, 2021;
originally announced August 2021.
-
Tight Polynomial Bounds for Loop Programs in Polynomial Space
Authors:
A. M. Ben-Amram,
G. W. Hamilton
Abstract:
We consider the following problem: given a program, find tight asymptotic bounds on the values of some variables at the end of the computation (or at any given program point) in terms of its input values. We focus on the case of polynomially-bounded variables, and on a weak programming language for which we have recently shown that tight bounds for polynomially-bounded variables are computable. Th…
▽ More
We consider the following problem: given a program, find tight asymptotic bounds on the values of some variables at the end of the computation (or at any given program point) in terms of its input values. We focus on the case of polynomially-bounded variables, and on a weak programming language for which we have recently shown that tight bounds for polynomially-bounded variables are computable. These bounds are sets of multivariate polynomials. While their computability has been settled, the complexity of this program-analysis problem remained open. In this paper, we show the problem to be PSPACE-complete. The main contribution is a new, space-efficient analysis algorithm. This algorithm is obtained in a few steps. First, we develop an algorithm for univariate bounds, a sub-problem which is already PSPACE-hard. Then, a decision procedure for multivariate bounds is achieved by reducing this problem to the univariate case; this reduction is orthogonal to the solution of the univariate problem and uses observations on the geometry of a set of vectors that represent multivariate bounds. Finally, we transform the univariate-bound algorithm to produce multivariate bounds.
△ Less
Submitted 10 November, 2021; v1 submitted 6 October, 2020;
originally announced October 2020.
-
Distilling Programs to Prove Termination
Authors:
G. W. Hamilton
Abstract:
The problem of determining whether or not any program terminates was shown to be undecidable by Turing, but recent advances in the area have allowed this information to be determined for a large class of programs. The classic method for deciding whether a program terminates dates back to Turing himself and involves finding a ranking function that maps a program state to a well-order, and then pro…
▽ More
The problem of determining whether or not any program terminates was shown to be undecidable by Turing, but recent advances in the area have allowed this information to be determined for a large class of programs. The classic method for deciding whether a program terminates dates back to Turing himself and involves finding a ranking function that maps a program state to a well-order, and then proving that the result of this function decreases for every possible program transition. More recent approaches to proving termination have involved moving away from the search for a single ranking function and toward a search for a set of ranking functions; this set is a choice of ranking functions and a disjunctive termination argument is used. In this paper, we describe a new technique for determining whether programs terminate. Our technique is applied to the output of the distillation program transformation that converts programs into a simplified form called distilled form. Programs in distilled form are converted into a corresponding labelled transition system and termination can be demonstrated by showing that all possible infinite traces through this labelled transition system would result in an infinite descent of well-founded data values. We demonstrate our technique on a number of examples, and compare it to previous work.
△ Less
Submitted 6 August, 2020;
originally announced August 2020.
-
Tight Polynomial Worst-Case Bounds for Loop Programs
Authors:
Amir M. Ben-Amram,
Geoff Hamilton
Abstract:
In 2008, Ben-Amram, Jones and Kristiansen showed that for a simple programming language - representing non-deterministic imperative programs with bounded loops, and arithmetics limited to addition and multiplication - it is possible to decide precisely whether a program has certain growth-rate properties, in particular whether a computed value, or the program's running time, has a polynomial growt…
▽ More
In 2008, Ben-Amram, Jones and Kristiansen showed that for a simple programming language - representing non-deterministic imperative programs with bounded loops, and arithmetics limited to addition and multiplication - it is possible to decide precisely whether a program has certain growth-rate properties, in particular whether a computed value, or the program's running time, has a polynomial growth rate.
A natural and intriguing problem was to move from answering the decision problem to giving a quantitative result, namely, a tight polynomial upper bound. This paper shows how to obtain asymptotically-tight, multivariate, disjunctive polynomial bounds for this class of programs. This is a complete solution: whenever a polynomial bound exists it will be found.
A pleasant surprise is that the algorithm is quite simple; but it relies on some subtle reasoning. An important ingredient in the proof is the forest factorization theorem, a strong structural result on homomorphisms into a finite monoid.
△ Less
Submitted 13 May, 2020; v1 submitted 24 June, 2019;
originally announced June 2019.
-
Generating Loop Invariants for Program Verification by Transformation
Authors:
G. W. Hamilton
Abstract:
Loop invariants play a central role in the verification of imperative programs. However, finding these invariants is often a difficult and time-consuming task for the programmer. We have previously shown how program transformation can be used to facilitate the verification of functional programs, but the verification of imperative programs is more challenging due to the need to discover these loop…
▽ More
Loop invariants play a central role in the verification of imperative programs. However, finding these invariants is often a difficult and time-consuming task for the programmer. We have previously shown how program transformation can be used to facilitate the verification of functional programs, but the verification of imperative programs is more challenging due to the need to discover these loop invariants. In this paper, we describe a technique for automatically discovering loop invariants. Our approach is similar to the induction-iteration method, but avoids the potentially exponential blow-up in clauses that can result when using this and other methods. Our approach makes use of the distil- lation program transformation algorithm to transform clauses into a simplified form that facilitates the identification of similarities and differences between them and thus help discover invariants. We prove that our technique terminates, and demonstrate its successful application to example programs that have proven to be problematic using other approaches. We also characterise the situations where our technique fails to find an invariant, and show how this can be ameliorated to a certain extent.
△ Less
Submitted 23 August, 2017;
originally announced August 2017.
-
Program Transformation to Identify List-Based Parallel Skeletons
Authors:
Venkatesh Kannan,
G. W. Hamilton
Abstract:
Algorithmic skeletons are used as building-blocks to ease the task of parallel programming by abstracting the details of parallel implementation from the developer. Most existing libraries provide implementations of skeletons that are defined over flat data types such as lists or arrays. However, skeleton-based parallel programming is still very challenging as it requires intricate analysis of the…
▽ More
Algorithmic skeletons are used as building-blocks to ease the task of parallel programming by abstracting the details of parallel implementation from the developer. Most existing libraries provide implementations of skeletons that are defined over flat data types such as lists or arrays. However, skeleton-based parallel programming is still very challenging as it requires intricate analysis of the underlying algorithm and often uses inefficient intermediate data structures. Further, the algorithmic structure of a given program may not match those of list-based skeletons. In this paper, we present a method to automatically transform any given program to one that is defined over a list and is more likely to contain instances of list-based skeletons. This facilitates the parallel execution of a transformed program using existing implementations of list-based parallel skeletons. Further, by using an existing transformation called distillation in conjunction with our method, we produce transformed programs that contain fewer inefficient intermediate data structures.
△ Less
Submitted 8 July, 2016;
originally announced July 2016.
-
Generating Counterexamples for Model Checking by Transformation
Authors:
G. W. Hamilton
Abstract:
Counterexamples explain why a desired temporal logic property fails to hold. The generation of counterexamples is considered to be one of the primary advantages of model checking as a verification technique. Furthermore, when model checking does succeed in verifying a property, there is typically no independently checkable witness that can be used as evidence for the verified property. Previously,…
▽ More
Counterexamples explain why a desired temporal logic property fails to hold. The generation of counterexamples is considered to be one of the primary advantages of model checking as a verification technique. Furthermore, when model checking does succeed in verifying a property, there is typically no independently checkable witness that can be used as evidence for the verified property. Previously, we have shown how program transformation techniques can be used for the verification of both safety and liveness properties of reactive systems. However, no counterexamples or witnesses were generated using the described techniques. In this paper, we address this issue. In particular, we show how the program transformation technique distillation can be used to facilitate the construction of counterexamples and witnesses for temporal properties of reactive systems. Example systems which are intended to model mutual exclusion are analysed using these techniques with respect to both safety (mutual exclusion) and liveness (non-starvation), with counterexamples being generated for those properties which do not hold.
△ Less
Submitted 8 July, 2016;
originally announced July 2016.
-
Proceedings of the Fourth International Workshop on Verification and Program Transformation
Authors:
Geoff Hamilton,
Alexei Lisitsa,
Andrei P. Nemytykh
Abstract:
This volume contains the revised versions of papers presented at the Fourth International Workshop on Verification and Program Transformation (VPT 2016) on April 2, 2016 in Eindhoven, The Netherlands. The workshop is an event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2016).
The aim of the VPT workshops is to provide a forum where people from the area of program…
▽ More
This volume contains the revised versions of papers presented at the Fourth International Workshop on Verification and Program Transformation (VPT 2016) on April 2, 2016 in Eindhoven, The Netherlands. The workshop is an event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2016).
The aim of the VPT workshops is to provide a forum where people from the area of program transformation and the area of program verification can fruitfully exchange ideas and gain a deeper understanding of the interactions between those two fields. The research papers which have been recently published in those fields, show that the interactions are very beneficial and, indeed, go both ways. In one direction, methods and tools developed in the field of program transformation, such as partial deduction, partial evaluation, fold/unfold transformations, and supercompilation, have all been applied with success for the verification of systems, and in particular, the verification of infinite state and parameterized systems. In the other direction, methods developed in program verification, such as model checking, abstract interpretation, SAT and SMT solving, and automated theorem proving, have been used to enhance program transformation techniques, thereby making these techniques more powerful and useful in practice.
△ Less
Submitted 6 July, 2016;
originally announced July 2016.
-
Verifying Temporal Properties of Reactive Systems by Transformation
Authors:
Geoff Hamilton
Abstract:
We show how program transformation techniques can be used for the verification of both safety and liveness properties of reactive systems. In particular, we show how the program transformation technique distillation can be used to transform reactive systems specified in a functional language into a simplified form that can subsequently be analysed to verify temporal properties of the systems. Exam…
▽ More
We show how program transformation techniques can be used for the verification of both safety and liveness properties of reactive systems. In particular, we show how the program transformation technique distillation can be used to transform reactive systems specified in a functional language into a simplified form that can subsequently be analysed to verify temporal properties of the systems. Example systems which are intended to model mutual exclusion are analysed using these techniques with respect to both safety (mutual exclusion) and liveness (non-starvation), with the errors they contain being correctly identified.
△ Less
Submitted 11 December, 2015;
originally announced December 2015.
