ABSTRACT. The paper is a contribution to exploring and analyzing space-improvements in the concurrent and functional process-calculus CHF. Space-improvements are defined as a generalization from a deterministic pure functional language. The main part of the paper is a polynomial algorithm for space optimizations of parallel independent processes. Applications of this algorithm are: (i) affirmation of space improving transformations for particular classes of program transformations; (ii) support of an interpreter-based method for refuting space-improvements; and (iii) as a stand-alone offline-optimizer for space (or similar ressources) of parallel processes.

ABSTRACT. A usual idea of transforming imperative programs over the integers into rewriting systems is to transform programs into transition systems where some auxiliary function symbols are introduced to represent intermediate states. In transforming a function calling itself or others, we allow an auxiliary symbol corresponding to a function call to have an extra argument where the called function is executed, and values stored in global variables are passed to the called function as its extra arguments, and the caller receives the possibly updated values together with returned values of the called function. Such a mechanism for global variables performs well under sequential execution, but is not enough to adapt to parallel execution. In this paper, we propose a transformation of imperative programs with function calls and global variables into logically constrained term rewriting systems that represent actions of the whole execution environment with call stacks. More precisely, we prepare a function symbol for the whole environment of execution, which stores global variables and a call stack as its arguments. For a function call, we push the frame to the stack and pop it after the execution. Any running frame is executed at the top of the stack, and statements accessing global variables are represented by rewrite rules for the environment symbol.

ABSTRACT. The grammar representation of a narrowing tree for a syntactically deterministic conditional term rewriting system and a pair of terms is a regular tree grammar that generates expressions for substitutions obtained by all possible innermost-narrowing derivations that start with the pair and end with non-narrowable terms. In this paper, under a certain syntactic condition, we show a transformation of the grammar representation of a narrowing tree into a regular tree grammar that generates the ranges of substitutions generated by the grammar representation. In our previous work, such a transformation is restricted to the ranges w.r.t.\ a given single variable, and thus, the usefulness is limited. We extend the previous transformation by considering the range of a substitution as a tuple of terms and by using the notion of coding for finite trees.

ABSTRACT. Our recently developed LRSX Tool implements a technique to automatically prove the correctness of program transformations in higher-order program calculi which may permit recursive let-bindings. The focused notion of correctness for program transformations is invariance with respect to the observational semantics of programs. The so-called diagram method is automated by combining unification, matching, and reasoning on alpha-renamings on the higher-order meta-language, and automating induction proofs via an encoding into termination problems of term rewrite systems. We explain the techniques, we illustrate the usage of the tool, and we report on experiments.

ABSTRACT. We give a language-parametric solution to the problem of total correctness, by automatically reducing it to the problem of partial correctness, under the assumption that a variant that decreases with each program step in a well-founded order is provided. Our approach assumes that the programming language semantics is given as a rewrite theory. We implement a prototype on top of the RMT tool and we show that it works in practice on a number of examples.

ABSTRACT. We propose AdaHorn, a model checker for verification of Ada programs wrt. correctness properties. AdaHorn translates Ada programs together with their related correctness properties into a set of Constrained Horn Clauses which are solved by well-known SMT solvers such as Eldarica and PDR-Z3. We propose a set of Ada programs inspired by C programs from the competition SV-COMP, and use them to compare the effectiveness of AdaHorn and GNATProve, a well-known static analyzer for Ada programs. Our experiments show that AdaHorn outperforms GNATProve by yielding correct results in more cases than GNATProve.