Search

Fortran is still widely used in scientific computing, and a very large corpus of legacy as well as new code is written in FORTRAN 77. In general this code is not type safe, so that incorrect programs can compile without errors. In this paper, we present a formal approach to ensure type safety of legacy Fortran code through automated program transformation. The objective of this work is to reduce programming errors by guaranteeing type safety. We present the first rigorous analysis of the type safety of FORTRAN 77 and the novel program transformation and type checking algorithms required to convert FORTRAN 77 subroutines and functions into pure, side-effect free subroutines and functions in Fortran 90. We have implemented these algorithms in a source-to-source compiler which type checks and automatically transforms the legacy code. We show that the resulting code is type safe and that the pure, side-effect free and referentially transparent subroutines can readily be offloaded to accelerators.

Nontransitive Noninterference (NTNI) and Nontransitive Types (NTT) are a new security condition and enforcement for policies which, in contrast to Denning's classical lattice model, assume no transitivity of the underlying flow relation. Nontransitive security policies are a natural fit for coarse-grained information-flow control where labels are specified at module rather than variable level of granularity. While the nontransitive and transitive policies pursue different goals and have different intuitions, this paper demonstrates that nontransitive noninterference can in fact be reduced to classical transitive noninterference. We develop a lattice encoding that establishes a precise relation between NTNI and classical noninterference. Our results make it possible to clearly position the new NTNI characterization with respect to the large body of work on noninterference. Further, we devise a lightweight program transformation that leverages standard flow-sensitive information-flow analyses to enforce nontransitive policies. We demonstrate several immediate benefits of our approach, both theoretical and practical. First, we improve the permissiveness over (while retaining the soundness of) the nonstandard NTT enforcement. Second, our results naturally generalize to a language with intermediate inputs and outputs. Finally, we demonstrate the practical benefits by utilizing state-of-the-art flow-sensitive tool JOANA to enforce nontransitive policies for Java programs.

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., Under consideration in Theory and Practice of Logic Programming (TPLP)

Despite decades of progress, static analysis tools still have great difficulty dealing with programs that combine arithmetic, loops, dynamic memory allocation, and linked data structures. In this paper we draw attention to two fundamental reasons for this difficulty: First, typical underlying program abstractions are low-level and inherently scalar, characterizing compound entities like data structures or results computed through iteration only indirectly. Second, to ensure termination, analyses typically project away the dimension of time, and merge information per program point, which incurs a loss in precision. As a remedy, we propose to make collective operations first-class in program analysis – inspired by Σ-notation in mathematics, and also by the success of high-level intermediate languages based on @map/reduce@ operations in program generators and aggressive optimizing compilers for domain-specific languages (DSLs). We further propose a novel structured heap abstraction that preserves a symbolic dimension of time, reflecting the program’s loop structure and thus unambiguously correlating multiple temporal points in the dynamic execution with a single point in the program text. This paper presents a formal model, based on a high-level intermediate analysis language, a practical realization in a prototype tool that analyzes C code, and an experimental evaluation that demonstrates competitive results on a series of benchmarks. Remarkably, our implementation achieves these results in a fully semantics-preserving strongest-postcondition model, which is a worst-case for analysis/verification. The underlying ideas, however, are not tied to this model and would equally apply in other settings, e.g., demand-driven invariant inference in a weakest-precondition model. Given its semantics-preserving nature, our implementation is not limited to analysis for verification, but can also check program equivalence, and translate legacy C code to high-performance DSLs.

Improving the performance of deep neural networks (DNNs) is important to both the compiler and neural architecture search (NAS) communities. Compilers apply program transformations in order to exploit hardware parallelism and memory hierarchy. However, legality concerns mean they fail to exploit the natural robustness of neural networks. In contrast, NAS techniques mutate networks by operations such as the grouping or bottlenecking of convolutions, exploiting the resilience of DNNs. In this work, we express such neural architecture operations as program transformations whose legality depends on a notion of representational capacity. This allows them to be combined with existing transformations into a unified optimization framework. This unification allows us to express existing NAS operations as combinations of simpler transformations. Crucially, it allows us to generate and explore new tensor convolutions. We prototyped the combined framework in TVM and were able to find optimizations across different DNNs, that significantly reduce inference time - over 3$\times$ in the majority of cases. Furthermore, our scheme dramatically reduces NAS search time. Code is available at~\href{https://github.com/jack-willturner/nas-as-program-transformation-exploration}{this https url}.

International audience; Tiling is a crucial program transformation, adjusting the ops-to-bytes balance of codes to improve locality. Like parallelism, it can be applied at multiple levels. Allowing tile sizes to be symbolic parameters at compile time has many benefits, including efficient autotuning, and run-time adaptability to system variations. For polyhedral programs, parametric tiling in its full generality is known to be non-linear, breaking the mathematical closure properties of the polyhedral model. Most compilation tools therefore either perform fixed size tiling, or apply parametric tiling in only the final, code generation step.We introduce monoparametric tiling, a restricted parametric tiling transformation. We show that, despite being parametric, it retains the closure properties of the polyhedral model. We first prove that applying monoparametric partitioning (i) to a polyhedron yields a union of polyhedra with modulo conditions, and (ii) to an affine function produces a piecewise-affine function with modulo conditions. We then use these properties to show how to tile an entire polyhedral program. Our monoparametric tiling is general enough to handle tiles with arbitrary tile shapes that can tessellate the iteration space (e.g., hexagonal, trapezoidal, etc). This enables a wide range of polyhedral analyses and transformations to be applied.

We consider the problem of automatically proving resource bounds. That is, we study how to prove that an integer-valued resource variable is bounded by a given program expression. Automatic resource-bound analysis has recently received significant attention because of a number of important applications (e.g., detecting performance bugs, preventing algorithmic-complexity attacks, identifying side-channel vulnerabilities), where the focus has often been on developing precise amortized reasoning techniques to infer the most exact resource usage. While such innovations remain critical, we observe that fully precise amortization is not always necessary to prove a bound of interest. And in fact, by amortizing selectively, the needed supporting invariants can be simpler, making the invariant inference task more feasible and predictable. We present a framework for selectively-amortized analysis that mixes worst-case and amortized reasoning via a property decomposition and a program transformation. We show that proving bounds in any such decomposition yields a sound resource bound in the original program, and we give an algorithm for selecting a reasonable decomposition.

We show how to systematically derive an efficient regular expression (regex) matcher using a variety of program transformation techniques, but very little specialized formal language and automata theory. Starting from the standard specification of the set-theoretic semantics of regular expressions, we proceed via a continuation-based backtracking matcher, to a classical, table-driven state machine. All steps of the development are supported by self-contained (and machine-verified) equational correctness proofs.

In this paper, we transform an orthogonal inductive definition set, which is a set of productions for inductive predicates, into a confluent term rewrite system such that a quantifier-free sequent is valid w.r.t. the inductive definition set if and only if an equation representing the sequent is an inductive theorem of the term rewrite system. To this end, we first propose a transformation of an orthogonal inductive definition set into a confluent term rewrite system that is equivalent to the inductive definition set in the sense of evaluating ground formulas. Then, we show that termination of the inductive definition set is proved by the generalized subterm criterion if and only if termination of the transformed term rewrite system is so. Finally, we show that the transformed term rewrite system with some rewrite rules for sequents has the expected property. In addition, we show a termination criterion for the union of term rewrite systems whose termination is proved by the generalized subterm criterion.

Models’ transformations involve code abstraction and program description, i.e., models’ transformations (MTs) operate in a more diverse set of artifacts than program transformation. Note that MTs allow programmers to link different structures, as Category Theory does for Mathematics, through recognizing similar features and properties. In this paper, we show that Category Theory can be used to describe MTs. Specifically, we propose a categorical framework for transforming a semi-structured data model, an OEM database, into a model of structured data, in UML language. This categorical approach allows us to establish a bridge between such models and the categories of simple and directed graphs, which makes it possible to apply the features of such categories to manage databases.

We introduce a language-independent framework for reasoning about program inverters by conditional term rewriting systems. These systems can model the three fundamental forms of inversion, i.e., full, partial and semi-inversion, in declarative languages. The correctness of the generic inversion algorithm introduced in this contribution is proven for all well-behaved rule inverters, and we demonstrate that this class of inverters encompasses several of the inversion algorithms published throughout the past years. This new generic approach enables us to establish fundamental properties, e.g., orthogonality, for entire classes of well-behaved full inverters, partial inverters and semi-inverters regardless of their particular local rule inverters. We study known inverters as well as classes of inverters that yield left-to-right deterministic systems; left-to-right determinism is a desirable property, e.g., for functional programs; however, at the same time it is not generally a property of inverted systems. This generic approach enables a more systematic design of program inverters and fills a gap in our knowledge of program inversion.

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., In Proceedings VPT/HCVS 2020, arXiv:2008.02483. This work owes a lot to the input of Neil Jones, who provided many useful insights and ideas on the subject matter presented here

© 2020 Copyright held by the owner/author(s). One of the workhorse techniques for implementing bottom-up Datalog engines is seminaïve evaluation. This optimization improves the performance of Datalog's most distinctive feature: recursively defined predicates. These are computed iteratively, and under a naïve evaluation strategy, each iteration recomputes all previous values. Seminaïve evaluation computes a safe approximation of the difference between iterations. This can asymptotically improve the performance of Datalog queries. Seminaïve evaluation is defined partly as a program transformation and partly as a modified iteration strategy, and takes advantage of the first-order nature of Datalog code. This paper extends the seminaïve transformation to higher-order programs written in the Datafun language, which extends Datalog with features like first-class relations, higher-order functions, and datatypes like sum types.

We address the problem of proving the satisfiability of Constrained Horn Clauses (CHCs) with Algebraic Data Types (ADTs), such as lists and trees. We propose a new technique for transforming CHCs with ADTs into CHCs where predicates are defined over basic types, such as integers and booleans, only. Thus, our technique avoids the explicit use of inductive proof rules during satisfiability proofs. The main extension over previous techniques for ADT removal is a new transformation rule, called differential replacement, which allows us to introduce auxiliary predicates corresponding to the lemmas that are often needed when making inductive proofs. We present an algorithm that uses the new rule, together with the traditional folding/unfolding transformation rules, for the automatic removal of ADTs. We prove that if the set of the transformed clauses is satisfiable, then so is the set of the original clauses. By an experimental evaluation, we show that the use of the differential replacement rule significantly improves the effectiveness of ADT removal, and we show that our transformation-based approach is competitive with respect to a well-established technique that extends the CVC4 solver with induction., 10th International Joint Conference on Automated Reasoning (IJCAR 2020) - version with appendix; added DOI of the final authenticated Springer publication; minor corrections

Backpropagation is a classic automatic differentiation algorithm computing the gradient of functions specified by a certain class of simple, first-order programs, called computational graphs. It is a fundamental tool in several fields, most notably machine learning, where it is the key for efficiently training (deep) neural networks. Recent years have witnessed the quick growth of a research field called differentiable programming, the aim of which is to express computational graphs more synthetically and modularly by resorting to actual programming languages endowed with control flow operators and higher-order combinators, such as map and fold. In this paper, we extend the backpropagation algorithm to a paradigmatic example of such a programming language: we define a compositional program transformation from the simply-typed lambda-calculus to itself augmented with a notion of linear negation, and prove that this computes the gradient of the source program with the same efficiency as first-order backpropagation. The transformation is completely effect-free and thus provides a purely logical understanding of the dynamics of backpropagation., Comment: 27 pages

Supercompilation is a powerful program transformation technique with numerous interesting applications. Existing methods of supercompilation, however, are often very unpredictable with respect to the size of the resulting programs. We consider an approach for controlling result size, based on a combination of multi-result supercompilation and a specific generalization strategy, which avoids code duplication. The current early experiments with this method show promising results - we can keep the size of the result small, while still performing powerful optimizations., Comment: In Proceedings VPT/HCVS 2020, arXiv:2008.02483. arXiv admin note: identical to arXiv:2006.02204, which has added appendices

In the article, we consider verification of programs with mutual recursion in the data driven functional parallel language Pifagor. In this language the program could be represented as a data flow graph, that has no control connections, and only has data relations. Under these conditions it is possible to simplify the process of formal verification, since there is no need to analyse resource conflicts, which are present in the systems with ordinary architectures. The proof of programs correctness is based on the elimination of mutual recursions by program transformation. The universal method of mutual recursion of an arbitrary number of functions elimination consists in constructing the universal recursive function that simulates all the functions in mutual recursion. A natural number is assigned to each function in mutual recursion. The universal recursive function takes as its argument the number of a function to be simulated and the arguments of this function. In some cases of the indirect recursion it is possible to use a simpler method of program transformation, namely, the merging of the functions code into a single function. To remove mutual recursion of an arbitrary number of functions, it is suggested to construct a graph of all connected functions and transform this graph by removing functions that are not connected with the target function, then by merging functions with indirect recursion and finally by constructing the universal recursive function. It is proved that in the Pifagor language such transformations of functions as code merging and universal recursive function construction do not change the correctness of the initial program. The example of partial correctness proof is given for the program that parses a simple arithmetic expression. We construct the graph of all connected functions and demonstrate two methods of proofs: by means of code merging and by means of the universal recursive function.

An improvement is a correct program transformation that optimizes the program, where the criterion is that the number of computation steps until a value is obtained is not strictly increased in any context. This paper investigates improvements in both – an untyped and a polymorphically typed variant – of a call-by-need lambda calculus with letrec, case, constructors and seq. Besides showing that several local transformations are optimizations, a main result of this paper is a proof that common subexpression elimination is correct and an improvement, which proves a conjecture and thus closes a gap in the improvement theory of Moran and Sands. The improvement relation used in this paper is generic in which essential computation steps are counted and thus the obtained results apply for several notions of improvement. Besides the small-step operational semantics, also an abstract machine semantics is considered for counting computation steps. We show for several length measures that the call-by-need calculus of Moran and Sands and our calculus are equivalent.

Staging allows a programmer to write domain-specific, custom code generators. Ideally, a programming language for staging provides all necessary features for staging, and at the same time, gives static guarantee for the safety properties of generated code including well typedness and well scopedness. We address this classic problem for the language with control operators, which allow code optimizations in a modular and compact way. Specifically, we design a staged programming language with the expressive control operators shift0 and reset0, which let us express, for instance, multi-layer let-insertion, while keeping the static guarantee of well typedness and well scopedness. For this purpose, we extend our earlier work on refined environment classifiers which were introduced for the staging language with state. We show that our language is expressive enough to express interesting code generation techniques, and that the type system enjoys type soundness. We also mention a type inference algorithm for our language under reasonable restriction.

Probabilistic programming systems make machine learning more modular by automating inference . Recent work by Shan and Ramsey makes inference more modular by automating conditioning . Their technique uses a symbolic program transformation that treats conditioning generally via the measure-theoretic notion of disintegration . This technique, however, is limited to conditioning a single scalar variable. As a step towards modular inference for realistic machine learning applications, we have extended the disintegration algorithm to symbolically condition arrays in probabilistic programs. The extended algorithm implements lifted disintegration , where repetition is treated symbolically and without unrolling loops. The technique uses a language of index variables for tracking expressions at various array levels. We find that the method works well for arbitrarily-sized arrays of independent random choices, with the conditioning step taking time linear in the number of indices needed to select an element.

It can be challenging to use algorithmic skeletons in parallel program development as it is tedious to manually identify parallel computations in an algorithm and there may be mismatches between the algorithm and skeletons. Also, parallel programs defined using skeletons often employ inefficient intermediate data structures. In this paper, we present a program transformation method to address these issues by using an existing technique called distillation to reduce the use of intermediate data structures and an encoding technique to combine the inputs of a program into a single input whose structure matches that of the program. This facilitates automatic identification of skeletons that suit the algorithmic structure of the transformed program.

We consider some extensions of co-logic programming and study its relationship with the Horn μ -calculus by Charatonik et al. We first consider negation elimination (NE) , a familiar technique of program transformation, for co-logic programs. Given a program P , NE derives its dual program P * which defines the “complement” of P . When we apply NE to co-logic programs with negation, we show that the stratification restriction, a syntactic condition imposed on co-logic programs, becomes too restrictive in general, and that the Horn μ -calculus can be used as an extension of co-logic programming for handling “non-stratified” co-logic programs. We then consider some applications of non-stratified co-logic programs to the well-founded semantics (WFS) and Answer Set Programming. In particular, we give new iterated fixpoint characterizations of the WFS as well as answer sets via dual programs. We also discuss some applications of non-stratified co-logic programs to program transformation such as partial deduction, and a proof procedure for the WFS.

Although functional as well as logic languages use equality to discriminate between logically different cases, the operational meaning of equality is different in such languages. Functional languages reduce equational expressions to their Boolean values, True or False, logic languages use unification to check the validity only and fail otherwise. Consequently, the language Curry, which amalgamates functional and logic programming features, offers two kinds of equational expressions so that the programmer has to distinguish between these uses. We show that this distinction can be avoided by providing an analysis and transformation method that automatically selects the appropriate operation. Without this distinction in source programs, the language design can be simplified and the execution of programs can be optimized. As a consequence, we show that one kind of equational expressions is sufficient and unification is nothing else than an optimization of Boolean equality.

Software watermarking is a defence technique used to prevent software piracy by embedding a signature, i.e., an identifier reliably representing the owner, in the code. When an illegal copy is made, the ownership can be claimed by extracting this identifier. The signature has to be hidden inside the program and it has to be difficult for an attacker to detect, tamper or remove it. In this paper we show how the ability of the attacker to identify the signature can be modelled in the framework of abstract interpretation as a completeness property. We view attackers as abstract interpreters that can precisely observe only the properties for which they are complete. In this setting, hiding a signature in the code corresponds to inserting it in terms of a semantic property that can be retrieved only by attackers that are complete for it. Indeed, any abstract interpreter that is not complete for the property specifying the signature cannot detect, tamper or remove it. The goal of this work is to introduce a formal framework for the modelling, at a semantic level, of software watermarking techniques and their quality features.

Recent years have witnessed a processor development trend that integrates central processing unit (CPU) and graphic processing unit (GPU) into a single chip. The integration helps to save some host-device data copying that a discrete GPU usually requires, but also introduces deep resource sharing and possible interference between CPU and GPU. This work investigates the performance implications of independently co-running CPU and GPU programs on these platforms. First, we perform a comprehensive measurement that covers a wide variety of factors, including processor architectures, operating systems, benchmarks, timing mechanisms, inputs, and power management schemes. These measurements reveal a number of surprising observations.We analyze these observations and produce a list of novel insights, including the important roles of operating system (OS) context switching and power management in determining the program performance, and the subtle effect of CPU-GPU data copying. Finally, we confirm those insights through case studies, and point out some promising directions to mitigate anomalous performance degradation on integrated heterogeneous processors.

Obfuscation is the art of making code hard to reverse engineer and understand. In this paper, we propose a formal model for specifying and understanding the strength of obfuscating transformations with respect to a given attack model. The idea is to consider the attacker as an abstract interpreter willing to extract information about the program’s semantics. In this scenario, we show that obfuscating code is making the analysis imprecise, namely making the corresponding abstract domain incomplete. It is known that completeness is a property of the abstract domain and the program to analyse. We introduce a framework for transforming abstract domains, i.e., analyses, towards incompleteness. The family of incomplete abstractions for a given program provides a characterisation of the potency of obfuscation employed in that program, i.e., its strength against the attack specified by those abstractions. We show this characterisation for known obfuscating transformations used to inhibit program slicing and automated disassembly.

Packet processing programs may have multiple semantically equivalent representations in terms of the match-action abstraction exposed by the underlying data plane. Some representations may encode the entire packet processing program into one large table allowing packets to be matched in a single lookup, while others may encode the same functionality decomposed into a pipeline of smaller match-action tables, maximizing modularity at the cost of increased lookup latency. In this paper, we provide the first systematic study of match-action program representations in order to assist network programmers in navigating this vast design space. Borrowing from relational database and formal language theory, we define a framework for the equivalent transformation of match-action programs to obtain certain irredundant representations that we call "normal forms". We find that normalization generally improves the capacity of the control plane to program the data-plane and to observe its state, at the same time having negligible, or positive, performance impact.

Inferring program transformations from concrete program changes has many potential uses, such as applying systematic program edits, refactoring, and automated program repair. Existing work for inferring program transformations usually rely on statistical information over a potentially large set of program-change examples. However, in many practical scenarios we do not have such a large set of program-change examples. In this paper, we address the challenge of inferring a program transformation from one single example. Our core insight is that "big code" can provide effective guide for the generalization of a concrete change into a program transformation, i.e., code elements appearing in many files are general and should not be abstracted away. We first propose a framework for transformation inference, where programs are represented as hypergraphs to enable fine-grained generalization of transformations. We then design a transformation inference approach, GENPAT, that infers a program transformation based on code context and statistics from a big code corpus. We have evaluated GENPAT under two distinct application scenarios, systematic editing and program repair. The evaluation on systematic editing shows that GENPAT significantly outperforms a state-of-the-art approach, SYDIT, with up to 5.5x correctly transformed cases. The evaluation on program repair suggests that GENPAT has the potential to be integrated in advanced program repair tools-GENPAT successfully repaired 19 real-world bugs in the Defects4J benchmark by simply applying transformations inferred from existing patches, where 4 bugs have never been repaired by any existing technique. Overall, the evaluation results suggest that GENPAT is effective for transformation inference and can potentially be adopted for many different applications.

The Static Single Assignment (SSA) form is an intermediate representation used for the analysis and optimization of programs in modern compilers. The ϕ-function placement is the most computationally expensive part of converting any program into its SSA form. The most widely-used ϕ-function placement algorithms are based on computing dominance frontiers. However, this kind of algorithms works under the limiting assumption that all variables are defined at the beginning of the program, which is not the case for local variables. In this paper, we introduce an innovative algorithm based on computing reaching definitions, only assuming that global variables and formal parameters are defined at the beginning of the program. We implemented our algorithm and compared it to a well-known dominance frontiers-based algorithm in the Clang/LLVM compiler framework by performing experiments on a benchmarking suite for Perl. The results of our experiments show that, besides a few computationally expensive cases, our algorithm is fairly efficient, and most notably it produces up to 169% and on an average 74% fewer ϕ-functions than the reference dominance frontiers-based algorithm.

In order to automatically infer the resource consumption of programs, analyzers track how data sizes change along program's execution. Typically, analyzers measure the sizes of data by applying norms which are mappings from data to natural numbers that represent the sizes of the corresponding data. When norms are defined by taking type information into account, they are named typed-norms. This article presents a transformational approach to resource analysis with typed-norms that are inferred by a data-flow analysis. The analysis is based on a transformation of the program into an intermediate abstract program in which each variable is abstracted with respect to all considered norms which are valid for its type. We also present the data-flow analysis to automatically infer the required, useful, typed-norms from programs. Our analysis is formalized on a simple rule-based representation to which programs written in different programming paradigms (e.g., functional, logic, imperative) can be automatically translated. Experimental results on standard benchmarks used by other type-based analyzers show that our approach is both efficient and accurate in practice. Under consideration in Theory and Practice of Logic Programming (TPLP)., Under consideration in Theory and Practice of Logic Programming (TPLP)

In this paper we present a novel approach to program optimisation based on compiler-based type-driven program transformations and a fast and accurate cost/performance model for the target architecture. We target streaming programs for the problem domain of scientific computing, such as numerical weather prediction. We present our theoretical framework for type-driven program transformation, our target high-level language and intermediate representation languages and the cost model and demonstrate the effectiveness of our approach by comparison with a commercial toolchain.

It is known that the verification of imperative, functional, and logic programs can be reduced to the satisfiability of constrained Horn clauses (CHCs), and this satisfiability check can be performed by using CHC solvers, such as Eldarica and Z3. These solvers perform well when they act on simple constraint theories, such as Linear Integer Arithmetic and the theory of Booleans, but their efficacy is very much reduced when the clauses refer to constraints on inductively defined structures, such as lists or trees. Recently, we have presented a transformation technique for eliminating those inductively defined data structures, and hence avoiding the need for incorporating induction principles into CHC solvers. However, this technique may fail when the transformation requires the use of lemmata whose generation needs ingenuity. In this paper we show, through an example, how during the process of transforming CHCs for eliminating inductively defined structures one can introduce suitable predicates, called difference predicates, whose definitions correspond to the lemmata to be introduced. Through a second example, we show that, whenever difference predicates cannot be introduced, we can introduce, instead, auxiliary queries which also correspond to lemmata, and the proof of these lemmata can be done by showing the satisfiability of those queries., Comment: In Proceedings VPT 2019, arXiv:1908.06723

It is well known that the areas of self-stabilizing algorithms and local algorithms are closely related. Using program transformation techniques local algorithms can be made self-stabilizing, albeit an increase in run-time or memory consumption is often unavoidable. Unfortunately these techniques often do not apply to randomized algorithms, which are often simpler and faster than deterministic algorithms. In this paper we demonstrate that it is possible to take over ideas from randomized distributed algorithms to self-stabilizing algorithms. We present two simple self-stabilizing algorithms computing a maximal independent set and a maximal matching and terminate in the synchronous model with high probability in \(O(\log n)\) rounds. The algorithms outperform all existing algorithms that do not rely on unique identifiers.

Traditional static resource analyses estimate the total resource usage of a program, without executing it. In this paper we present a novel resource analysis whose aim is instead the static profiling of accumulated cost, i.e., to discover, for selected parts of the program, an estimate or bound of the resource usage accumulated in each of those parts. Traditional resource analyses are parametric in the sense that the results can be functions on input data sizes. Our static profiling is also parametric, i.e., our accumulated cost estimates are also parameterized by input data sizes. Our proposal is based on the concept of cost centers and a program transformation that allows the static inference of functions that return bounds on these accumulated costs depending on input data sizes, for each cost center of interest. Such information is much more useful to the software developer than the traditional resource usage functions, as it allows identifying the parts of a program that should be optimized, because of their greater impact on the total cost of program executions. We also report on our implementation of the proposed technique using the CiaoPP program analysis framework, and provide some experimental results. This paper is under consideration for acceptance in TPLP., Paper presented at the 32nd International Conference on Logic Programming (ICLP 2016), New York City, USA, 16-21 October 2016, 22 pages, LaTeX

This paper presents a technique to model ping-pong protocols by prefix grammars in such a way that the security of the protocol models becomes decidable by a general-purpose program transformation tool with unfolding. The presented approach not only decides whether a protocol model is insecure but also builds a set of possible attack models explicitly.

We present a principled modular approach to the development of construction and verification tools for imperative programs, in which the control flow and the data flow are cleanly separated. Our simplest verification tool uses Kleene algebra with tests for the control flow of while-programs and their standard relational semantics for the data flow. It is expanded to a basic program construction tool by adding an operation for the specification statement and one single axiom. To include recursive procedures, Kleene algebras with tests are expanded further to quantales with tests. In this more expressive setting, iteration and the specification statement can be defined explicitly and stronger program transformation rules can be derived. Programming our approach in the Isabelle/HOL interactive theorem prover yields simple lightweight mathematical components as well as program construction and verification tools that are correct by construction themselves. Verification condition generation and program construction rules are based on equational reasoning and supported by powerful Isabelle tactics and automated theorem proving. A number of examples shows our tools at work.

Probabilistic Logic Programs (PLPs) generalize traditional logic programs and allow the encoding of models combining logical structure and uncertainty. In PLP, inference is performed by summarizing the possible worlds which entail the query in a suitable data structure, and using this data structure to compute the answer probability. Systems such as ProbLog, PITA, etc., use propositional data structures like explanation graphs, BDDs, SDDs, etc., to represent the possible worlds. While this approach saves inference time due to substructure sharing, there are a number of problems where a more compact data structure is possible. We propose a data structure called Ordered Symbolic Derivation Diagram (OSDD) which captures the possible worlds by means of constraint formulas. We describe a program transformation technique to construct OSDDs via query evaluation, and give procedures to perform exact and approximate inference over OSDDs. Our approach has two key properties. Firstly, the exact inference procedure is a generalization of traditional inference, and results in speedup over the latter in certain settings. Secondly, the approximate technique is a generalization of likelihood weighting in Bayesian Networks, and allows us to perform sampling-based inference with lower rejection rate and variance. We evaluate the effectiveness of the proposed techniques through experiments on several problems.

We address the problem of verifying the satisfiability of Constrained Horn Clauses (CHCs) based on theories of inductively defined data structures, such as lists and trees. We propose a transformation technique whose objective is the removal of these data structures from CHCs, hence reducing their satisfiability to a satisfiability problem for CHCs on integers and booleans. We propose a transformation algorithm and identify a class of clauses where it always succeeds. We also consider an extension of that algorithm, which combines clause transformation with reasoning on integer constraints. Via an experimental evaluation we show that our technique greatly improves the effectiveness of applying the Z3 solver to CHCs. We also show that our verification technique based on CHC transformation followed by CHC solving, is competitive with respect to CHC solvers extended with induction. This paper is under consideration for acceptance in TPLP., Paper presented at the 34nd International Conference on Logic Programming (ICLP 2018), Oxford, UK, July 14 to July 17, 2018. 22 pages, LaTeX

The paper describes how to verify cryptographic protocols by a general-purpose programtransformation technique with unfolding. The questions of representation and analysisof the protocols as prefix rewriting grammars are discussed. In these aspects Higman andTurchin embeddings on computational paths are considered, and a refinement of Turchin’srelation is presented that allows to algorithmically decide the empty word problem forprefix rewriting grammars.

The paper describes a verification technique based on program transformation with unfolding. The technique allows to find short attacks on multi-party ping-pong protocols in the Dolev–Yao intruder model. Protocols are modelled by prefix grammars, and questions of model optimization and complexity are considered. Examples of model programs for protocols were written in a functional language and were analyzed by a general-purpose supercompiler.

As a rule, program transformation methods based on semantics unfolda semantic tree of a given program. Sometimes that allows to optimize the program or to prove its certain properties automatically.Unfolding is one of the basic operations, which is a meta-extension of one step of the abstract machine executing the program.This paper is interested in unfolding for programs based on pattern matching and manipulating the strings. The corresponding computation model originates from Markov's normal algorithms and extends this theoretical base.Even though algorithms unfolding programs were being intensively studied for a long time in the context of variety of programming languages, as far as we know, the associative concatenation was stood at the wayside of the stream.We define a class of term rewriting systems manipulating with strings anddescribe an algorithm unfolding the programs from the class. The programming language defined by this class is algorithmic complete.Given a word equation, one of the algorithms suggested in this paper results in a description of the corresponding solution set.

When implementing a programming language, we often write a parser and a pretty-printer. However, manually writing both programs is not only tedious but also error-prone; it may happen that a pretty-printed result is not correctly parsed. In this paper, we propose FliPpr, which is a program transformation system that uses program inversion to produce a CFG parser from a pretty-printer. This novel approach has the advantages of fine-grained control over pretty-printing, and easy reuse of existing efficient pretty-printer and parser implementations.

During the last decade we have designed several tools for assisting the development of flexible software applications coded with a promising language in the fuzzy logic programming area. In the so-called multi-adjoint logic programming approach, a set of logic rules are assembled with a set of fuzzy connective definitions (whose truth functions are defined as functional rules) for manipulating truth degrees beyond the simpler case of {true,false}. Moreover, we have recently provided optimization techniques by reusing some variants of program transformation techniques based on unfolding which have been largely exploited in the pure functional -not fuzzy- setting for enhancing the behavior of such operators. In this paper we experimentally show the benefits of using the new c-unfolding transformation applied on fuzzy connectives and how to improve the efficiency of the proper unfolding process by reusing the very well-known concept of dependency graph. Moreover, we accompany our technique with cost analysis and discussions on practical aspects.

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., Comment: Paper presented at the 34nd International Conference on Logic Programming (ICLP 2018), Oxford, UK, July 14 to July 17, 2018 18 pages, LaTeX

Semantics-preserving program transformations, such as those carried out by an optimizing compiler, can affect the results of static program analyses. In the best cases, a transformation increases precision or allows a simpler analysis to replace a complex one. In other cases, transformations have the opposite effect, reducing precision. This work constructs a theoretical framework to analyze this intriguing phenomenon. The framework provides a simple, uniform explanation for precision changes, linking them to bisimulation relations that justify the correctness of a transformation. It offers a mechanism for recovering lost precision through the systematic construction of a new, bisimulating analysis. Furthermore, it is shown that program analyses defined over a class of composite domains can be factored into a program transformation followed by simpler, equally precise analyses of the target program.

This paper presents the implementation of a program transformation that removes square roots and divisions from functional programs without recursion, producing code that can be exactly computed. This transformation accepts different subsets of languages as input and it provides a certifying mechanism when the targeted language is Pvs. In this case, we provide a relation between every function definition in the output code and its corresponding one in the input code, that specifies the behavior of the produced function with respect to the input one. This transformation has been implemented in OCaml and has been tested on different algorithms from the NASA ACCoRD project.

We present a method for verifying properties of imperative programs that manipulate integer arrays. Imperative programs and their properties are represented by using Constraint Logic Programs (CLP) over integer arrays. Our method is refutational. Given a Hoare triple {phi} prog {psi} that defines a partial correctness property of an imperative program prog, we encode the negation of the property as a predicate incorrect defined by a CLP program P, and we show that the property holds by proving that incorrect is not a consequence of P. Program verification is performed by applying a sequence of semantics preserving transformation rules and deriving a new CLP program T such that incorrect is a consequence of P iff it is a consequence of T. The rules are applied according to an automatic strategy whose objective is to derive a program T that satisfies one of the following properties: either (i) T is the empty set of clauses, hence proving that incorrect does not hold and prog is correct, or (ii) T contains the fact incorrect, hence proving that prog is incorrect. Our transformation strategy makes use of an axiomatization of the theory of arrays for the manipulation of array constraints, and also applies the widening and convex hull operators for the generalization of linear integer constraints. The strategy has been implemented in the VeriMAP transformation system and it has been shown to be quite effective and efficient on a set of benchmark array programs taken from the literature.

In order to achieve competitive performance, abstract machines for Prolog and related languages end up being large and intricate, and incorporate sophisticated optimizations, both at the design and at the implementation levels. At the same time, efficiency considerations make it necessary to use low-level languages in their implementation. This makes them laborious to code, optimize, and, especially, maintain and extend. Writing the abstract machine (and ancillary code) in a higher-level language can help tame this inherent complexity. We show how the semantics of most basic components of an efficient virtual machine for Prolog can be described using (a variant of) Prolog. These descriptions are then compiled to C and assembled to build a complete bytecode emulator. Thanks to the high level of the language used and its closeness to Prolog, the abstract machine description can be manipulated using standard Prolog compilation and optimization techniques with relative ease. We also show how, by applying program transformations selectively, we obtain abstract machine implementations whose performance can match and even exceed that of state-of-the-art, highly-tuned, hand-crafted emulators., 56 pages, 46 figures, 5 tables, To appear in Theory and Practice of Logic Programming (TPLP)

We focus on synthesis techniques for transforming existing fault-intolerant real-time programs into fault-tolerant programs that provide phased recovery . A fault-tolerant program is one that satisfies its safety and liveness specifications as well as timing constraints in the presence of faults. We argue that in many commonly considered programs (especially in safety/mission-critical systems), when faults occur, simple recovery to the program’s normal behavior is necessary, but not sufficient. For such programs, it is necessary that recovery is accomplished in a sequence of phases, each ensuring that the program satisfies certain properties. In the simplest case, in the first phase the program recovers to an acceptable behavior within some time θ , and, in the second phase, it recovers to the ideal behavior within time δ . In this article, we introduce four different types of bounded-time 2-phase recovery, namely ordered-strict, strict, relaxed, and graceful, based on how a real-time fault-tolerant program reaches the acceptable and ideal behaviors in the presence of faults. We rigorously analyze the complexity of automated synthesis of each type: we either show that the problem is hard in some class of complexity or we present a sound and complete synthesis algorithm. We argue that such complexity analysis is essential to deal with the highly complex decision procedures of program synthesis.