1 citations · 1 across the 4 of their papers we have counts for
4 papers
Termination of Innermost-Terminating Right-Linear Overlay Term Rewrite Systems
Naoki Nishida
It has been shown that, regarding a terminating right-linear overlay term rewrite system (TRS), any rewrite sequence terminating in a normal form can be simulated by an innermost r…
Rewriting Induction for Existentially Quantified Equations in Logically Constrained Rewriting (Full Version)
Naoki Nishida, Kazushi Nishie, Misaki Kojima
Rewriting Induction (RI) is a principle to prove that an equation over terms is an inductive theorem of a rewrite system, i.e., that any ground instance of the equation is a theore…
Abstract Framework for All-Path Reachability Analysis toward Safety and Liveness Verification (Full Version)
Misaki Kojima, Naoki Nishida
An All-Path Reachability 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…
Difference of Constrained Patterns in Logically Constrained Term Rewrite Systems (Full Version)
Naoki Nishida, Misaki Kojima, Yuto Nakamura
Considering patterns as sets of their instances, a difference operator over patterns computes a finite set of two given patterns, which represents the difference between the divide…