This article aims to develop a verification method for procedural programs via transformation into logically constrained term rewriting systems (LCTRSs). To this end, we extend methods based on integer handle arbitrary data types, global variables, function calls, and arrays, encode safety checks. Then adapt existing induction LCTRSs propose simple yet effective generalize equations. We show that can automatically verify memory prove correctness of realistic functions. Our approach proves...

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 considered function is tail recursive. this paper, we propose direct intuitive approach to recursive functions. Our new technique able produce good results even without...

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

An all-path reachability (APR, for short) problem of a logically constrained term rewrite system (LCTRS, is pair terms representing state sets. APR demonically valid if every finite execution path from any in the first set to an irreducible includes second set. We have proposed framework reduce non-occurrence specified error states transition represented by LCTRS with constant destinations. In this paper, focusing on quasi-termination narrowing, we characterize class LCTRSs which problems...

Given a constructor term rewriting system that defines injective functions, the inversion compiler proposed by Nishida, Sakai and Sakabe generates conditional inverse relations of then unravels into an unconditional system. In general, resulting is not (innermost-)confluent even if (innermost-)confluent. this paper, we propose modification Knuth-Bendix completion procedure, which used as post-processor compiler. confluent operationally terminating system, procedure takes systems input. When...

Essentially, in a reversible programming language, for each forward computation step from state S to S', there exists a constructive and deterministic method go backwards S' to S. Besides its theoretical interest, reversible computation is fundamental concept which relevant many different areas like cellular automata, bidirectional program transformation, or quantum computing, name few. In this paper, we focus on term rewriting, computation model that underlies most rule-based...

Term rewriting systems (TRSs) extended by allowing to contain extra variables in their rewrite rules are called EV-TRSs. They ill-natured since every one-step reduction with is infinitely branching and they not terminating. To solve these problems, this paper shows that narrowing can simulate sequences of EV-TRSs as starting from ground terms. We prove the soundness for sequences. completeness case right-linear systems, also any redex reduced sequence introduced means variables. Moreover, we...