From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting. - Misaki Kojima; Naoki Nishida 001 (PADL, 2023)

On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic. - Ayuka Matsumi; Naoki Nishida 001; Misaki Kojima; Donghoon Shin (CoRR, 2023)

Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting. - Misaki Kojima; Naoki Nishida 001 (J. Log. Algebraic Methods Program., 2023)

On Solving All-Path Reachability Problems for Starvation Freedom of Concurrent Rewrite Systems Under Process Fairness. - Misaki Kojima; Naoki Nishida 001 (RP, 2024)

A Sufficient Condition of Logically Constrained Term Rewrite Systems for Decidability of All-path Reachability Problems with Constant Destinations. - Misaki Kojima; Naoki Nishida 001 (J. Inf. Process., 2024)

Transforming concurrent programs with semaphores into logically constrained term rewrite systems. - Misaki Kojima; Naoki Nishida 001; Yutaka Matsubara (J. Log. Algebraic Methods Program., 2025)

Transforming imperative programs into bisimilar logically constrained term rewrite systems via injective functions from configurations to terms. - Naoki Nishida 001; Misaki Kojima; Takumi Kato (J. Log. Algebraic Methods Program., 2025)

A nesting-preserving transformation of SIMP programs into logically constrained term rewrite systems. - Naoki Nishida 001; Misaki Kojima; Ayuka Matsumi (J. Log. Algebraic Methods Program., 2025)

Difference of Constrained Patterns in Logically Constrained Term Rewrite Systems (Full Version). - Naoki Nishida 001; Misaki Kojima; Yuto Nakamura (CoRR, 2025)