35 citations · 65 across the 12 of their papers we have counts for
7 papers · 1 filter
On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic
Ayuka Matsumi, Naoki Nishida, Misaki Kojima +1
As for term rewrite systems, the dependency pair (DP, for short) framework with several kinds of DP processors is useful for proving termination of logically constrained term rewri…
On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions
Naoki Nishida, Yuya Maeda
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 expr…
On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems
Yoshiaki Kanazawa, Naoki Nishida
In this paper, we show a new approach to transformations of an imperative program with function calls and global variables into a logically constrained term rewriting system. The r…
Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers
Tomohiro Sasano, Naoki Nishida, Masahiko Sakai +1
In the dependency pair framework for proving termination of rewriting systems, polynomial interpretations are used to transform dependency chains into bounded decreasing sequences…
Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction
Shinnosuke Mizutani, Naoki Nishida
A proof tableau of Hoare logic is an annotated program with pre- and post-conditions, which corresponds to an inference tree of Hoare logic. In this paper, we show that a proof tab…
Verifying Procedural Programs via Constrained Rewriting Induction
Carsten Fuhs, Cynthia Kop, Naoki Nishida
This paper aims to develop a verification method for procedural programs via a transformation into Logically Constrained Term Rewriting Systems (LCTRSs). To this end, we extend tra…
Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity
Naoki Nishida, Masahiko Sakai, Toshiki Sakabe
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)…