Faculty Profiles - NISHIDA Naoki

Papers - NISHIDA Naoki

Division display 1 - 20 of about 249 ／ All the affair displays >>

On Transforming Prioritized Multithreaded Programs into Logically Constrained Term Rewrite Systems Reviewed

Misaki Kojima and Naoki Nishida

Informal Proceedings of the 11th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2025) page： 39 - 51 2025.7

Authorship：Last author,　Corresponding author Language：English Publishing type：Research paper (international conference proceedings)

A transformation of multithreaded programs without priorities into logically constrained term rewrite systems (LCTRS, for short) has been proposed. In this paper, we extend it to prioritized threads by introducing a descending list of priorities into terms representing configurations. As a case study, we show a verification example in which a runtime-error verification method based on all-path reachability detects an assertion failure caused by the interrupt of a high-priority thread.

On Merging Constrained Rewrite Rules of Induction Hypotheses in Constrained Rewriting Induction Reviewed

Naoki Nishida and Nozomi Taira

Informal Proceedings of the 11th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2025) page： 85 - 96 2025.7

Authorship：Lead author,　Last author,　Corresponding author Language：English Publishing type：Research paper (international conference proceedings)

In proving constrained equations by rewriting induction (RI, for short), the Expand rule which is one of the main inference rules of RI makes an orientable constrained equation a constrained rewrite rule, called an IH rewrite rule, which can be used as an induction hypothesis. Such an IH rewrite rule may be applied to constrained equations in order to simplify them. The broader the scope of the application of IH rewrite rules, the greater the possibilities for proving constrained equations. In this paper, we modify the Expand rule of RI in order to make the scope of the application of the IH rewrite rule broader. To be more precise, in orienting a constrained equation as an IH rewrite rule, if there already exists an IH rewrite rule having the same left- and right-hand sides, then we disjunct the constraint of the orienting equation with the constraint of the existing IH rewrite rule; otherwise, the orienting equation is added to the set of IH rewrite rules as a new IH rewrite rule. We show that this modification does not lose the proof power of RI.

Transforming imperative programs into bisimilar logically constrained term rewrite systems via injective functions from configurations to terms Reviewed International journal

Naoki Nishida, Misaki Kojima, and Takumi Kato

Journal of Logical and Algebraic Methods in Programming Vol. 145 page： 1 - 18 2025.5

Authorship：Lead author,　Corresponding author Language：English Publishing type：Research paper (scientific journal) Publisher：Elsevier

To transform an imperative program into a logically constrained term rewrite system (LCTRS, for short), previous work transforms a list of statements into rewrite rules in a stepwise manner, and proves the correctness along the transformation and the big-step semantics of the program. On the other hand, the small-step semantics of a programming language consists of inference rules that define single transitions of configurations. Partial instances of such inference rules are almost the same as rewrite rules in the transformed LCTRS. In this paper, we aim at establishing a framework for simpler definitions and correctness proofs of transformations from programs into LCTRSs. To this end, for the transformation in previous work as an example, we show the existence of an injective function from configurations of a given program to terms, and reformulate the transformation by means of the injective function. The injective function enables us to make a one-to-one correspondence between single small-step transitions and reduction steps, and provides bisimilarity between the program and transformed LCTRS, resulting in a simpler correctness proof.

DOI： 10.1016/j.jlamp.2025.101056

A nesting-preserving transformation of SIMP programs into logically constrained term rewrite systems Reviewed International journal

Naoki Nishida, Misaki Kojima, and Ayuka Matsumi

Journal of Logical and Algebraic Methods in Programming Vol. 144 page： 1 - 15 2025.3

Authorship：Lead author,　Corresponding author Language：English Publishing type：Research paper (scientific journal) Publisher：Elsevier

In the last decade, several transformations of an imperative program into a logically constrained term rewrite system (LCTRS, for short) have been investigated and extended. They do not preserve the nesting of statements, generating rewrite rules like transition systems, while function calls are represented by the nesting of function symbols. Structural features of the original program must often be useful in analyzing the transformed LCTRS. To use such features, we have to know how to transform the program into the LCTRS by keeping the correspondence between statements in the program and the introduced auxiliary function symbols in the LCTRS, or by transforming the LCTRS into a control flow graph to, e.g., recover loop information. In this paper, we propose a nesting-preserving transformation of a SIMP program (a C-like integer program) into an LCTRS. The transformation is mostly based on previous work and introduces the nesting of function symbols that correspond to the nesting of statements in the original program. To be more precise, we propose a construction of a tree homomorphism which is used as a post-process of the transformation in previous work, i.e., which is applied to the LCTRS obtained from the program. As a correctness statement for the nesting-preserving transformation, we show that the tree homomorphism is sound and complete for the reduction of the LCTRS.

DOI： 10.1016/j.jlamp.2025.101045

Transforming concurrent programs with semaphores into logically constrained term rewrite systems Reviewed International journal

Misaki Kojima, Naoki Nishida, Yutaka Matsubara

Journal of Logical and Algebraic Methods in Programming Vol. 143 page： 1 - 23 2025.2

Authorship：Corresponding author Language：English Publishing type：Research paper (scientific journal) Publisher：Elsevier

In this paper, as a first step of modeling concurrent programs by logically constrained term rewrite systems (LCTRSs, for short), we show transformations of concurrent programs with semaphore-based exclusive control into LCTRSs. To this end, we show how to encode configurations of concurrent programs with a fixed number of processes. Then, we show how to encode some well-known operations for semaphores by rewrite rules, showing two transformations of concurrent programs with semaphores into LCTRSs. We adopt list-using and list-free approaches to the encoding of waiting queues for semaphores in LCTRSs. While the former straightforwardly uses lists, the latter uses a so-called take-a-number system in order to avoid using any recursive data structures for waiting queues.

DOI： 10.1016/j.jlamp.2024.101033

On Solving All-Path Reachability Problems for Starvation Freedom of Concurrent Rewrite Systems Under Process Fairness Reviewed International journal

Misaki Kojima and Naoki Nishida

Proceedings of the 18th International Conference on Reachability Problems (RP 2024) Vol. 15050 page： 54 - 70 2024.9

Authorship：Last author,　Corresponding author Language：English Publishing type：Research paper (international conference proceedings) Publisher：Springe, Cham

Logically constrained term rewrite systems are useful models of not only sequential but also concurrent programs. We have proposed a framework to soundly reduce starvation freedom of a concurrent program to an all-path reachability problem of the corresponding logically constrained term rewrite system, where process fairness is not considered. In this paper, we show a disproof criterion for starvation freedom and then extend the framework to starvation freedom under process fairness.

DOI： 10.1007/978-3-031-72621-7_5

On completeness of decomposion of equations with disjunctive constraints on provability of constrained rewriting induction

Nozomi Taira, Naoki Nishida, and Masahiko Sakai

Record of 2024 Tokai-Section Joint Conference on Electrical, Electronics, Information, and Related Engineering ( H6-4 ) page： 1 2024.8

CRaris: CR checker for LCTRSs in ARI Style

Naoki Nishida and Misaki Kojima

Proceedings of the 13th International Workshop on Confluence page： 83 - 84 2024.7

On Proving Confluence of Concurrent Programs by All-Path Reachability of LCTRSs Reviewed

Misaki Kojima and Naoki Nishida

Proceedings of the 13th International Workshop on Confluence page： 2 - 8 2024.7

Authorship：Last author,　Corresponding author Language：English Publishing type：Research paper (conference, symposium, etc.)

A logically constrained term rewrite system (LCTRS, for short) modeling a concurrent program is usually non-terminating, left-linear, and overlapping, but sometimes confluent w.r.t. an initial ground term which corresponds to an initial configuration of the program. In this paper, we show how to prove confluence of such an LCTRS w.r.t. the initial term. To be more precise, we add the rule from the initial term to a fresh constant to the LCTRS, and construct a proof tree for the all-path reachability problem from the initial term to the constant. If the directed graph obtained from the proof tree by considering it as a cyclic proof is strongly connected and each node corresponds to a single term, then all terms reachable from the initial term can be reduced back to the initial one and thus the original LCTRS is confluent w.r.t. the initial one.

CO3 (Version 2.5)

Naoki Nishida and Misaki Kojima

Proceedings of the 13th International Workshop on Confluence page： 71 - 72 2024.7

Confluence Competition 2024 International coauthorship

Raul Gutierrez, Aart Middeldorp, Naoki Nishida, Teppai Saito, and Rene Thiemann

Proceedings of the 13th International Workshop on Confluence page： 63 - 64 2024.7

Equational Theories and Validity for Logically Constrained Term Rewriting Reviewed International coauthorship

Takahito Aoto, Naoki Nishida, and Jonas Schöpf

Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2018), LIPIcs Vol. 299 page： 31:1 - 31:21 2024.7

Authorship：Lead author Language：English Publishing type：Research paper (international conference proceedings)

Logically constrained term rewriting is a relatively new formalism where rules are equipped with constraints over some arbitrary theory. Although there are many recent advances with respect to rewriting induction, completion, complexity analysis and confluence analysis for logically constrained term rewriting, these works solely focus on the syntactic side of the formalism lacking detailed investigations on semantics. In this paper, we investigate a semantic side of logically constrained term rewriting. To this end, we first define constrained equations, constrained equational theories and validity of the former based on the latter. After presenting the relationship of validity and conversion of rewriting, we then construct a sound inference system to prove validity of constrained equations in constrained equational theories. Finally, we give an algebraic semantics, which enables one to establish invalidity of constrained equations in constrained equational theories. This algebraic semantics derives a new notion of consistency for constrained equational theories.

DOI： 10.4230/LIPIcs.FSCD.2024.31

A Sufficient Condition of Logically Constrained Term Rewrite Systems for Decidability of All-path Reachability Problems with Constant Destinations Reviewed International journal

Misaki Kojima and Naoki Nishida

Journal of Information Processing Vol. 32 page： 417 - 435 2024.5

Authorship：Last author,　Corresponding author Language：English Publishing type：Research paper (scientific journal) Publisher：Information Processing Society of Japan

An all-path reachability (APR, for short) problem of a logically constrained term rewrite system (LCTRS, for short) is a pair of constrained terms representing state sets. An APR problem is demonically valid if every finite execution path from any state in the first set to an irreducible state includes a state in the second set. We have proposed a framework to reduce the non-occurrence of specified error states in a transition system represented by an LCTRS to an APR problem with irreducible constant destinations. In this paper, by focusing on quasi-termination of constrained narrowing, we characterize a class of LCTRSs of which APR problems with constant destinations are decidable. Quasi-termination of a (constrained) term w.r.t. narrowing is the finiteness of the set of reachable narrowed (constrained) terms from the initial (constrained) term up to variable renaming (and equivalence of constraints). To this end, we first introduce an inference rule for disproofs to a proof system for APR problems with constant destinations and formulate (dis)proof trees of APR problems in the style of cyclic proofs. Secondly, to prove correctness of disproof trees, we adapt constrained narrowing to LCTRSs and show soundness of constrained narrowing of LCTRSs w.r.t. constrained rewriting. Thirdly, we show a sufficient condition of LCTRSs for quasi-termination of constrained narrowing starting from linear constrained terms that have no nesting of defined symbols: Rewrite rules are right-linear and nesting-free w.r.t. defined symbols, and the application of rewrite rules for (mutually) recursive defined symbols does not increase the height of resulting constrained terms of narrowing. Finally, we show that if a constrained term is quasi-terminating w.r.t. narrowing of an LCTRS over a sort-wise finite signature with a decidable theory, then the APR problem consisting of the constrained term and an irreducible constant is decidable.

DOI： 10.2197/ipsjjip.32.417

Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting Reviewed International journal

Misaki Kojima and Naoki Nishida

Journal of Logical and Algebraic Methods in Programming Vol. 135 page： 1 - 19 2023.10

Authorship：Last author,　Corresponding author Language：English Publishing type：Research paper (scientific journal)

A concurrent program with semaphore-based exclusive control can be modeled by a logically constrained term rewrite system. In this paper, we first propose a framework to reduce the non-occurrence of a specified runtime error in the program to an all-path reachability problem of the transformed logically constrained term rewrite system. Here, an all-path reachability problem of the system is a pair of state sets and is demonically valid if every finite execution path starting with a state in the first set and ending with a terminating state includes a state in the second set. Then, we propose a weakened but easily-implementable variant of an existing proof system for all-path reachability problems. As a case study, we deal with the race freedom of concurrent programs with semaphore-based exclusive control.

DOI： 10.1016/j.jlamp.2023.100903

On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic Reviewed

Ayuka Mastumi, Naoki Nishida, Misaki Kojima, and Donghoon Shin

Proceedings of the 19th International Workshop on Termination page： 1 - 6 2023.8

Authorship：Last author,　Corresponding author Language：English Publishing type：Research paper (conference, symposium, etc.)

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 rewrite systems (LCTRSs, for short). However, the polynomial interpretation processor is not so effective against LCTRSs with bit-vector arithmetic (BV-LCTRSs, for short). In this paper, we propose a novel DP processor for BV-LCTRSs to solve a singleton DP problem consisting of a dependency pair forming a self-loop. The processor is based on an acyclic directed graph such that the nodes are bit-vectors and any dependency chain of the problem is projected to a path of the graph. We show a sufficient condition for the existence of such an acyclic graph, and simplify it for a specific case.

DOI： 10.48550/arXiv.2307.14094

CO3 (Version 2.4)

Naoki Nishida, Misaki Kojima, and Ayuka Matsumi

Proceedings of the 12th International Workshop on Confluence page： 67 2023.8

A New Format for Rewrite Systems Reviewed International coauthorship

Takahito Aoto, Nao Hirokawa, Dohan Kim, Misaki Kojima, Aart Middeldorp, Fabian Mitterwallner, Naoki Nishida, Teppei Saito, Jonas Schöpf, Kiraku Shintani, Rene Thiemann, and Akihisa Yamada

Proceedings of the 12th International Workshop on Confluence page： 32 - 37 2023.8

Confluence Competition 2023 International coauthorship

Raul Gutierrez, Aart Middeldorp, Naoki Nishida, and Kiraku Shintani

Proceedings of the 12th International Workshop on Confluence page： 61 - 62 2023.8

On Representations of Waiting Queues for Semaphores in Logically Constrained Term Rewrite Systems Reviewed

Misaki Kojima and Naoki Nishida

Informal Proceedings of the 10th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2023) page： 1 - 6 2023.7

Authorship：Last author,　Corresponding author Language：English Publishing type：Research paper (international conference proceedings)

A transformation of concurrent programs with semaphore-based exclusive control and waiting queues into logically constrained term rewrite systems (LCTRSs, for short) has been proposed. To represent waiting queues, the transformation adopts a turn waiting system with number tickets, while the use of usual lists is a straightforward approach. In this abstract, we show a list-based approach to waiting queues and compare the two approaches by means of verification of race freedom of a simple reader-writer example.

A Nesting-Preserving Transformation of SIMP Programs into Logically Constrained Term Rewrite Systems Reviewed

Naoki Nishida, Misaki Kojima, and Ayuka Matsumi

Informal Proceedings of the 10th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2023) page： 1 - 11 2023.7

Authorship：Last author,　Corresponding author Language：English Publishing type：Research paper (international conference proceedings)

In the last decade, several transformations of an imperative program into a logically constrained term rewrite system (LCTRS, for short) have been investigated and extended. They do not preserve the nesting of statements, generating rewrite rules like transition systems, while function calls are represented by the nesting of function symbols. Structural features of the original program must be often useful in analyzing the transformed LCTRS, but, to use such features, we have to know how to transform the program into the LCTRS, e.g., we keep the correspondence between statements in the program and the introduced auxiliary function symbols in the LCTRS. In this paper, we propose a nesting-preserving transformation of a SIMP program (a C integer program) into an LCTRS. The transformation is almost based on previous work and introduces the nesting of function symbols that correspond to statements in the original program. To be more precise, we propose a construction of a tree homomorphism which is used as a post-process of the transformation in previous work, i.e., which is applied to the LCTRS obtained from the program. As a correctness of the nesting-preserving transformation, we show that the tree homomorphism is sound and complete for the reduction of the LCTRS.

　 PREV - NEXT 　

<NISHIDA Naoki>

Papers - NISHIDA Naoki