Naoki Nishida

76 papers A 2B 6C 11Misc 3Journal 32Unranked 20
YearRankTypeTitle / Venue / Authors
2026 J jnl
Abstract Framework for All-Path Reachability Analysis toward Safety and Liveness Verification (Full Version).
CoRR
Misaki Kojima, Naoki Nishida
2026 J jnl
Partial Rewriting and Value Interpretation of Logically Constrained Terms (Full Version).
CoRR
Takahito Aoto, Naoki Nishida, Jonas Schöpf
2026 J jnl
Rewriting Induction for Existentially Quantified Equations in Logically Constrained Rewriting (Full Version).
CoRR
Naoki Nishida, Kazushi Nishie, Misaki Kojima
2025 J jnl
A nesting-preserving transformation of SIMP programs into logically constrained term rewrite systems.
J. Log. Algebraic Methods Program.
Naoki Nishida, Misaki Kojima, Ayuka Matsumi
2025 J jnl
Characterizing Equivalence of Logically Constrained Terms via Existentially Constrained Terms (Full Version).
CoRR
Kanta Takahata, Jonas Schöpf, Naoki Nishida, Takahito Aoto
2025 C conf
Characterizing Equivalence of Logically Constrained Terms via Existentially Constrained Terms.
LOPSTR
Kanta Takahata, Jonas Schöpf, Naoki Nishida, Takahito Aoto
2025 J jnl
Difference of Constrained Patterns in Logically Constrained Term Rewrite Systems (Full Version).
CoRR
Naoki Nishida, Misaki Kojima, Yuto Nakamura
2025 — conf
Difference of Constrained Patterns in Logically Constrained Term Rewrite Systems.
FroCoS
Naoki Nishida, Misaki Kojima, Yuto Nakamura
2025 J jnl
Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations (Full Version).
CoRR
Kanta Takahata, Jonas Schöpf, Naoki Nishida, Takahito Aoto
2025 C conf
Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations.
PPDP
Kanta Takahata, Jonas Schöpf, Naoki Nishida, Takahito Aoto
2025 J jnl
Transforming concurrent programs with semaphores into logically constrained term rewrite systems.
J. Log. Algebraic Methods Program.
Misaki Kojima, Naoki Nishida, Yutaka Matsubara
2025 J jnl
Transforming imperative programs into bisimilar logically constrained term rewrite systems via injective functions from configurations to terms.
J. Log. Algebraic Methods Program.
Naoki Nishida, Misaki Kojima, Takumi Kato
2024 J jnl
A Sufficient Condition of Logically Constrained Term Rewrite Systems for Decidability of All-path Reachability Problems with Constant Destinations.
J. Inf. Process.
Misaki Kojima, Naoki Nishida
2024 J jnl
Equational Theories and Validity for Logically Constrained Term Rewriting (Full Version).
CoRR
Takahito Aoto, Naoki Nishida, Jonas Schöpf
2024 B conf
Equational Theories and Validity for Logically Constrained Term Rewriting.
FSCD
Takahito Aoto, Naoki Nishida, Jonas Schöpf
2024 — conf
On Solving All-Path Reachability Problems for Starvation Freedom of Concurrent Rewrite Systems Under Process Fairness.
RP
Misaki Kojima, Naoki Nishida
2023 C conf
From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting.
PADL
Misaki Kojima, Naoki Nishida
2023 J jnl
On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic.
CoRR
Ayuka Matsumi, Naoki Nishida, Misaki Kojima, Donghoon Shin
2023 J jnl
Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting.
J. Log. Algebraic Methods Program.
Misaki Kojima, Naoki Nishida
2022 Misc conf
On Transforming Cut- and Quantifier-Free Cyclic Proofs into Rewriting-Induction Proofs.
FLOPS
Shujun Zhang, Naoki Nishida
2022 J jnl
Transforming orthogonal inductive definition sets into confluent term rewrite systems.
J. Log. Algebraic Methods Program.
Shujun Zhang, Naoki Nishida
2021 J jnl
Determinization of inverted grammar programs via context-free expressions.
J. Log. Algebraic Methods Program.
Naoki Nishida, Minami Niwa
2021 J jnl
Reversible CSP Computations.
IEEE Trans. Parallel Distributed Syst.
Carlos Galindo, Naoki Nishida, Josep Silva, Salvador Tamarit
2020 — ch.
A Case Study for Reversible Computing: Reversible Debugging of Concurrent Programs.
Selected Results of the COST Action IC1405
James Hoey, Ivan Lanese, Naoki Nishida, Irek Ulidowski, Germán Vidal
2020 C conf
ReverCSP: Time-Travelling in CSP Computations.
RC
Carlos Galindo, Naoki Nishida, Josep Silva, Salvador Tamarit
2019 C conf
Characterizing Compatible View Updates in Syntactic Bidirectionalization.
RC
Naoki Nishida, Germán Vidal
2018 J jnl
A Theory of Reversibility for Erlang.
CoRR
Ivan Lanese, Naoki Nishida, Adrián Palacios, Germán Vidal
2018 J jnl
A theory of reversibility for Erlang.
J. Log. Algebraic Methods Program.
Ivan Lanese, Naoki Nishida, Adrián Palacios, Germán Vidal
2018 Misc conf
CauDEr: A Causal-Consistent Reversible Debugger for Erlang.
FLOPS
Ivan Lanese, Naoki Nishida, Adrián Palacios, Germán Vidal
2018 B conf
Confluence Competition 2018.
FSCD
Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, Harald Zankl
2018 — conf
Loop Detection by Logically Constrained Term Rewriting.
VSTTE
Naoki Nishida, Sarah Winkler
2018 B conf
Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems.
FSCD
Naoki Nishida, Yuya Maeda
2018 — conf
On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems.
WPTE@FSCD
Yoshiaki Kanazawa, Naoki Nishida
2018 — conf
On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions.
WPTE@FSCD
Naoki Nishida, Yuya Maeda
2018 J jnl
Reversible computation in term rewriting.
J. Log. Algebraic Methods Program.
Naoki Nishida, Adrián Palacios, Germán Vidal
2018 J jnl
Rewriting induction for constrained inequalities.
Sci. Comput. Program.
Takahiro Nagao, Naoki Nishida
2017 J jnl
Relative Termination via Dependency Pairs.
J. Autom. Reason.
José Iborra, Naoki Nishida, Germán Vidal, Akihisa Yamada
2017 J jnl
Reversible Computation in Term Rewriting.
CoRR
Naoki Nishida, Adrián Palacios, Germán Vidal
2017 — conf
Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers.
WPTE@FSCD
Tomohiro Sasano, Naoki Nishida, Masahiko Sakai, Tomoya Ueyama
2017 — conf
Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction.
WPTE@FSCD
Shinnosuke Mizutani, Naoki Nishida
2017 J jnl
Verifying Procedural Programs via Constrained Rewriting Induction.
ACM Trans. Comput. Log.
Carsten Fuhs, Cynthia Kop, Naoki Nishida
2016 C conf
A Reversible Semantics for Erlang.
LOPSTR
Naoki Nishida, Adrián Palacios, Germán Vidal
2016 C conf
Proving inductive validity of constrained inequalities.
PPDP
Takahiro Nagao, Naoki Nishida
2016 B conf
Reversible Term Rewriting.
FSCD
Naoki Nishida, Adrián Palacios, Germán Vidal
2016 — conf
Sound Structure-Preserving Transformation for Weakly-Left-Linear Deterministic Conditional Term Rewriting Systems.
WPTE@FSCD
Ryota Nakayama, Naoki Nishida, Masahiko Sakai
2016 J jnl
Towards Reversible Computation in Erlang.
CoRR
Naoki Nishida, Adrián Palacios, Germán Vidal
2015 — ed.
2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE@RDP 2015, Warsaw, Poland, July 2, 2015
WPTE@RDP
Yuki Chiba, Santiago Escobar, Naoki Nishida, David Sabel, Manfred Schmidt-Schauß
2015 J jnl
A framework for computing finite SLD trees.
J. Log. Algebraic Methods Program.
Naoki Nishida, Germán Vidal
2015 A conf
Confluence Competition 2015.
CADE
Takahito Aoto, Nao Hirokawa, Julian Nagele, Naoki Nishida, Harald Zankl
2015 B conf
Constrained Term Rewriting tooL.
LPAR
Cynthia Kop, Naoki Nishida
2015 A conf
Reducing Relative Termination to Dependency Pair Problems.
CADE
José Iborra, Naoki Nishida, Germán Vidal, Akihisa Yamada
2014 B conf
Automatic Constrained Rewriting Induction towards Verifying Procedural Programs.
APLAS
Cynthia Kop, Naoki Nishida
2014 J jnl
Conversion to tail recursion in term rewriting.
J. Log. Algebraic Methods Program.
Naoki Nishida, Germán Vidal
2014 — conf
Inverse Unfold Problem and Its Heuristic Solving.
WPTE@RTA/TLCA
Masanori Nagashima, Tomofumi Kato, Masahiko Sakai, Naoki Nishida
2014 — conf
Notes on Structure-Preserving Transformations of Conditional Term Rewrite Systems.
WPTE@RTA/TLCA
Karl Gmeiner, Naoki Nishida
2014 — conf
On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings.
WPTE@RTA/TLCA
Naoki Nishida, Makishi Yanagisawa, Karl Gmeiner
2014 J jnl
Towards Verifying Procedural Programs using Constrained Rewriting Induction.
CoRR
Cynthia Kop, Naoki Nishida
2013 C conf
A Finite Representation of the Narrowing Space.
LOPSTR
Naoki Nishida, Germán Vidal
2013 — conf
On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms.
TTATT
Naoki Nishida, Masahiko Sakai, Yasuhiro Nakano
2013 — conf
Term Rewriting with Logical Constraints.
FroCos
Cynthia Kop, Naoki Nishida
2012 J jnl
A Sound Type System for Typing Runtime Errors.
Inf. Media Technol.
Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe, Masahiko Sakai, Naoki Nishida
2012 C conf
Computing More Specific Versions of Conditional Rewriting Systems.
LOPSTR
Naoki Nishida, Germán Vidal
2012 C conf
Improving Determinization of Grammar Programs for Program Inversion.
LOPSTR
Minami Niwa, Naoki Nishida, Masahiko Sakai
2012 J jnl
Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity
Log. Methods Comput. Sci.
Naoki Nishida, Masahiko Sakai, Toshiki Sakabe
2011 J jnl
Decidability of Reachability for Right-shallow Context-sensitive Term Rewriting Systems.
Inf. Media Technol.
Yoshiharu Kojima, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, Toshiki Sakabe
2011 — conf
On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs.
WFLP
Tsubasa Sakata, Naoki Nishida, Toshiki Sakabe
2011 — conf
Program Inversion for Tail Recursive Functions.
RTA
Naoki Nishida, Germán Vidal
2011 — conf
Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity.
RTA
Naoki Nishida, Masahiko Sakai, Toshiki Sakabe
2010 Misc conf
Proving Injectivity of Functions via Program Inversion in Term Rewriting.
FLOPS
Naoki Nishida, Masahiko Sakai
2010 J jnl
Termination of narrowing via termination of rewriting.
Appl. Algebra Eng. Commun. Comput.
Naoki Nishida, Germán Vidal
2009 J jnl
Context-sensitive Innermost Reachability is Decidable for Linear Right-shallow Term Rewriting Systems.
Inf. Media Technol.
Yoshiharu Kojima, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, Toshiki Sakabe
2009 C conf
Goal-Directed and Relative Dependency Pairs for Proving the Termination of Narrowing.
LOPSTR
José Iborra, Naoki Nishida, Germán Vidal
2008 — conf
Completion after Program Inversion of Injective Functions.
WRS@RTA
Naoki Nishida, Masahiko Sakai
2006 — conf
Transformation for Refining Unraveled Conditional Term Rewriting Systems.
WRS@FLoC
Naoki Nishida, Tomohiro Mizutani, Masahiko Sakai
2005 — conf
Partial Inversion of Constructor Term Rewriting Systems.
RTA
Naoki Nishida, Masahiko Sakai, Toshiki Sakabe
2003 — conf
Narrowing-based simulation of term rewriting systems with extra variables.
WFLP
Naoki Nishida, Masahiko Sakai, Toshiki Sakabe