An all-path reachability (APR, for short) predicate over an object set is a pair of a source set and a target set, which are subsets of the object set. APR predicates have been defined for abstract reduction systems (ARSs, for short) and then extended to logically constrained term rewrite systems (LCTRSs, for short) as pairs of constrained terms that represent sets of terms modeling configurations, states, etc. An APR predicate is partially (or demonically) valid w.r.t. a rewrite system if every finite maximal reduction sequence of the system starting from any element in the source set includes an element in the target set. Partial validity of APR predicates w.r.t. ARSs is defined by means of two inference rules, which can be considered a proof system to construct (possibly infinite) derivation trees for partial validity. On the other hand, a proof system for LCTRSs consists of four inference rules, leaving a gap between the inference rules for ARSs and LCTRSs. In this paper, we revisit the framework for APR analysis and adapt it to verification of not only safety but also liveness properties. To this end, we first reformulate an abstract framework for partial validity w.r.t. ARSs so that there is a one-to-one correspondence between the inference rules for partial validity w.r.t. ARSs and LCTRSs. Secondly, we show how to apply APR analysis to safety verification. Thirdly, to apply APR analysis to liveness verification, we introduce a novel stronger validity of APR predicates, called total validity, which requires not only finite but also infinite execution paths to reach target sets. Finally, for a partially valid APR predicate with a cyclic-proof tree, we show that the acyclicity of the proof graph obtained from the cyclic-proof tree is a necessary and sufficient condition for total validity. The condition implies that if there exists a cyclic-proof tree for an APR predicate, the proof graph of which is acyclic, then the APR predicate is totally valid.

Logically constrained term rewriting is a relatively new rewriting formalism that naturally supports built-in data structures, such as integers and bit vectors. In the analysis of logically constrained term rewrite systems (LCTRSs), rewriting constrained terms plays a crucial role. However, this combines rewrite rule applications and equivalence transformations in a closely intertwined way. This intertwining makes it difficult to establish useful theoretical properties for this kind of rewriting and causes problems in implementations—namely, that impractically large search spaces are often required. To address this issue, we propose in this paper a novel notion of most general constrained rewriting, which operates on existentially constrained terms, a concept recently introduced by the authors. We define a class of left-linear, left-value-free LCTRSs that are general enough to simulate all left-linear LCTRSs and exhibit the desired key property: most general constrained rewriting commutes with equivalence. This property ensures that equivalence transformations can be deferred until after the application of rewrite rules, which helps mitigate the issue of large search spaces in implementations. In addition to that, we show that the original rewriting formalism on constrained terms can be embedded into our new rewriting formalism on existentially constrained terms. Thus, our results are expected to have significant implications for achieving correct and efficient implementations in tools operating on LCTRSs.

Logically constrained term rewriting is a relatively new formalism where rules are equipped with constraints over some arbitrary theory. Although there are many recent advances with respect to rewriting induction, completion, complexity analysis and confluence analysis for logically constrained term rewriting, these works solely focus on the syntactic side of the formalism lacking detailed investigations on semantics. In this paper, we investigate a semantic side of logically constrained term rewriting. To this end, we first define constrained equations, constrained equational theories and validity of the former based on the latter. After presenting the relationship of validity and conversion of rewriting, we then construct a sound inference system to prove validity of constrained equations in constrained equational theories. Finally, we give an algebraic semantics, which enables one to establish invalidity of constrained equations in constrained equational theories. This algebraic semantics derive a new notion of consistency for constrained equational theories.

Reversibility enables a program to be executed both forwards and backwards. This ability allows programmers to backtrack the execution to a previous state. This is essential if the computation is not deterministic because re-running the program forwards may not lead to that state of interest. Reversibility of sequential programs has been well studied and a strong theoretical basis exists. Contrarily, reversibility of concurrent programs is still very young, especially in the practical side. For instance, in the particular case of the Communicating Sequential Processes (CSP) language, reversibility is practically missing. In this article, we present a new technique, including its formal definition and its implementation, to reverse CSP computations. Most of the ideas presented can be directly applied to other concurrent specification languages such as Promela or CCS, but we center the discussion and the implementation on CSP. The technique proposes different forms of reversibility, including strict reversibility and causal-consistent reversibility. On the practical side, we provide an implementation of a system to reverse CSP computations that is able to highlight the source code that is being executed in each forwards/backwards computation step, and that has been optimized to be scalable to real systems.

A term rewrite system is terminating when no infinite reduction sequences are possible. Relative termination generalizes termination by permitting infinite reductions as long as some distinguished rules are not applied infinitely many times. Relative termination is thus a fundamental notion that has been used in a number of different contexts, like analyzing the confluence of rewrite systems or the termination of narrowing. In this work, we introduce a novel technique to prove relative termination by reducing it to dependency pair problems. To the best of our knowledge, this is the first significant contribution to Problem #106 of the RTA List of Open Problems. We first present a general approach that is then instantiated to provide a concrete technique for proving relative termination. The practical significance of our method is illustrated by means of an experimental evaluation.

This article aims to develop a verification method for procedural programs via a transformation into logically constrained term rewriting systems (LCTRSs). To this end, we extend transformation methods based on integer term rewriting systems to handle arbitrary data types, global variables, function calls, and arrays, and to encode safety checks. Then we adapt existing rewriting induction methods to LCTRSs and propose a simple yet effective method to generalize equations. We show that we can automatically verify memory safety and prove correctness of realistic functions. Our approach proves equivalence between two implementations; thus, in contrast to other works, we do not require an explicit specification in a separate specification language.

Rewriting induction (RI) frameworks consist of inference rules to prove equations to be inductive theorems of a given term rewriting system, i.e., to be inductively valid w.r.t. reduction of the given system. To prove inductive validity of inequalities within such frameworks, one may reduce inequalities to equations. However, it is often hard to prove inductive validity of such reduced equations within the existing RI frameworks due to their indirect handling of inequalities. In this paper, we adapt the notion of inductive theorems to inequalities and propose an RI framework for directly proving inductive validity of inequalities of constrained term rewriting systems. Within the framework, we handle inequalities that may contain function symbols defined in a given rewriting system but not necessarily interpreted by the built-in semantics. Direct handling of inequalities facilitates the utilization of transitivity of magnitude relations via inequalities obtained as induction hypotheses. Our approach succeeds in proving inductive validity of some inequalities that are hard to verify within the existing RI frameworks for equations.

Unravelings are transformations from a conditional term rewriting system (CTRS, for short) over an original signature into an unconditional term rewriting systems (TRS, for short) over an extended signature. They are not sound for every CTRS w.r.t. reduction, while they are complete w.r.t. reduction. Here, soundness w.r.t. reduction means that every reduction sequence of the corresponding unraveled TRS, of which the initial and end terms are over the original signature, can be simulated by the reduction of the original CTRS. In this paper, we show that an optimized variant of Ohlebusch's unraveling for deterministic CTRSs is sound w.r.t. reduction if the corresponding unraveled TRSs are left-linear or both right-linear and non-erasing. We also show that soundness of the variant implies that of Ohlebusch's unraveling.

Program inversion is a fundamental problem that has been addressed in many different programming settings and applications. In the context of term rewriting, several methods already exist for computing the inverse of an injective function. These methods, however, usually return non-terminating inverted functions when the considered function is tail recursive. In this paper, we propose a direct and intuitive approach to the inversion of tail recursive functions. Our new technique is able to produce good results even without the use of an additional post-processing of determinization or completion. Moreover, when combined with a traditional approach to program inversion, it constitutes a promising approach to define a general method for program inversion. Our experimental results confirm that the new technique compares well with previous approaches.