Faculty Profiles - NISHIDA Naoki

Papers - NISHIDA Naoki

Division display 21 - 40 of about 247 ／ All the affair displays >>

Naoki Nishida and Misaki Kojima

Proceedings of the 11th International Workshop on Confluence page： 63 2022.8

Confluence Competition 2022 International coauthorship

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

Proceedings of the 11th International Workshop on Confluence page： 54 2022.8

On Transforming Imperative Programs into Logically Constrained Term Rewrite Systems via Injective Functions from Configurations to Terms Reviewed

Naoki Nishida, Misaki Kojima, and Takumi Kato

Informal Proceedings of the 9th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2022) page： 1 - 16 2022.7

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

To transform an imperative program into a logically constrained term rewrite system (LCTRS, for short), previous work converts a statement list to rewrite rules in a stepwise manner, and proves the correctness along such a conversion and the big-step semantics of the program. On the other hand, the small-step semantics of a programming language comprises of inference rules that define transition steps 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 plain definitions and correctness proofs of transformations from programs into LCTRSs. To this end, for the transformation in previous work, we show an injective function from configurations to terms, and reformulate the transformation by means of the injective function. The injective function maps a transition step to a reduction step, and results in a plain correctness proof.

On Reducing Non-Occurrence of Specified Runtime Errors to All-Path Reachability Problems of Constrained Rewriting Reviewed

Misaki Kojima and Naoki Nishida

Informal Proceedings of the 9th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2022) page： 1 - 16 2022.7

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

A concurrent program with semaphore-based exclusive control can be transformed into a logically constrained term rewrite system that is computationally equivalent to the program. 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 is a pair of state sets and is true 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, as a case study, we show how to apply the framework to the race-freeness of semaphore-based exclusive control in the program. Finally, we show a simplified variant of a proof system for all-path reachability problems.

On Transforming Rewriting-Induction Proofs for Logical-Connective-Free Sequents into Cyclic Proofs Reviewed

Shujun Zhang and Naoki Nishida

Informal Proceedings of the 9th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2022) page： 1 - 14 2022.7

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

A GSC-terminating and orthogonal inductive definition set (IDS, for short) of first-order predicate logic can be transformed into a many-sorted term rewrite system (TRS, for short) such that a quantifier-free sequent is valid w.r.t. the IDS if and only if a term equation representing the sequent is an inductive theorem of the TRS. Under certain assumptions, it has been shown that a quantifier- and cut-free cyclic proof of a sequent can be transformed into a rewriting-induction (RI, for short) proof of the corresponding term equation. The RI proof can be transformed back into the cyclic proof, but it is not known how to transform arbitrary RI proofs into cyclic proofs. In this paper, we show that for a quantifier- and logical-connective-free sequent, if there exists an RI proof of the corresponding term equation, then there exists a cyclic proof of some sequent w.r.t. some IDS such that the cyclic proof ensures the validity of the initial sequent. To this end, we show a transformation of the RI proof into such a cyclic proof, a sequent, and an IDS.

Transforming orthogonal inductive definition sets into confluent term rewrite systems Reviewed International journal

Shujun Zhang and Naoki Nishida

Journal of Logical and Algebraic Methods in Programming Vol. 127 page： 1 - 17 2022.6

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

In this paper, we transform an orthogonal inductive definition set, which is a set of productions for inductive predicates, into a confluent term rewrite system such that a quantifier-free sequent is valid w.r.t. the inductive definition set if and only if an equation representing the sequent is an inductive theorem of the term rewrite system. To this end, we first propose a transformation of an orthogonal inductive definition set into a confluent term rewrite system that is equivalent to the inductive definition set in the sense of evaluating ground formulas. Then, we show that termination of the inductive definition set is proved by the generalized subterm criterion if and only if termination of the transformed term rewrite system is so. Finally, we show that the transformed term rewrite system with some rewrite rules for sequents has the expected property. In addition, we show a termination criterion for the union of term rewrite systems whose termination is proved by the generalized subterm criterion.

DOI： 10.1016/j.jlamp.2022.100779

On Transforming Cut- and Quantifier-Free Cyclic Proofs into Rewriting-Induction Proofs Reviewed International journal

Shujun Zhang and Naoki Nishida

Proceedings of the 16th International Symposium on Functional and Logic Programming (FLOPS 2022), Lecture Notes in Computer Science Vol. 13215 page： 262 - 281 2022.5

Authorship：Corresponding author Language：English Publishing type：Research paper (international conference proceedings) Publisher：Springer

An inductive definition set (IDS, for short) of first-order predicate logic can be transformed into a many-sorted term rewrite system (TRS, for short) such that a quantifier-free sequent is valid w.r.t. the IDS if and only if a term equation representing the sequent is an inductive theorem of the TRS. In this paper, to compare rewriting induction (RI, for short) with cyclic proof systems, under certain assumptions, we show that if a sequent has a cut- and quantifier-free cyclic proof, then there exists an RI proof for a term equation of the sequent. To this end, we propose a transformation of a cut- and quantifier-free cyclic proof of the sequent into an RI proof for the corresponding equation.

DOI： 10.1007/978-3-030-99461-7_15

Implementing Determinization of Term Rewrite Systems via Equivalence of Context-Free Expressions Toward Program Inversion

Himika Kumagai and Naoki Nishida

Record of the 84th National Convention of IPSJ page： 271 - 272 2022.3

On Constrained Rewrite Rules Representing Semantics Rules of LLVM IR

Takumi Kato, Naoki Nishida, and Masahiko Sakai

IEICE Technical Rerport Vol. 121 ( 318 ) page： 89 - 94 2022.1

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

A method to verify programs written in a simple C-like language via logically constrained term rewrite systems (LCTRS, for short) has been investigated. The method transforms a program into an LCTRS, and reduces properties of the program to those of the transformed LCTRS. In this article, we propose a transformation of LLVM IRs into LCTRSs, aiming at expanding the scope of the method. In the semantics of LLVM IRs, a configuration includes a memory and an assignment as mappings in general. On the other hand, LCTRSs used in the existing work do not deal with such mappings as built-in data, and thus, function symbols keep ranges of memories and assignments as arguments, making the transformation and its correctness proof more complicated. For this reason, we employ LCTRSs that deal with memories and assignments as built-in data, as LLVM IRs do. This makes a correctness proof of our transformation clear. More precisely, we define an injective mapping from configurations to terms. Using the mapping, we propose a transformation that generates a rewrite rule for each instruction in an LLVM IR by instantiating each inference rule of the LLVM-IR semantics which is applicable to the instruction.

Lemma Generation by Lagrange Interpolation in Con- strained Rewriting Induction

Shinya Higa, Naoki Nishida, and Masahiko Sakai

Proceedings of the 38th Conference of Japan Society for Software Science and Technology page： 1 - 13 2021.9

Determinization of inverted grammar programs via context-free expressions Reviewed International journal

Naoki Nishida and Minami Niwa

Journal of Logical and Algebraic Methods in Programming Vol. 122 page： 1 - 26 2021.8

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

In a reversible language, any forward computation can be undone by a finite sequence of backward steps. Reversible computing has been studied in the context of different programming languages and formalisms, where it has been used for testing and verifica- tion, among others. In this paper, we consider a subset of Erlang, a functional and concurrent programming language based on the actor model. We present a formal semantics for reversible computation in this language and prove its main properties, including its causal consistency. We also build on top of it a rollback operator that can be used to undo the actions of a process up to a given checkpoint.

DOI： 10.1016/j.jlamp.2021.100688

Other Link： http://hdl.handle.net/2237/0002001914

Confluence Competition 2021 International coauthorship

Aart Middeldorp, Naoki Nishida, Kiraku Shintani, and Johannes Waldmann

Proceedings of the 10th International Workshop on Confluence page： 51 2021.7

CO3 (Version 2.2)

Naoki Nishida

Proceedings of the 10th International Workshop on Confluence page： 61 2021.7

On Transforming Inductive Definition Sets into Term Rewrite Systems Reviewed

Shujun Zhang and Naoki Nishida

Informal Proceedings of the 8th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2021) page： 1 - 10 2021.7

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

In this paper, we transform an inductive definition set—a set of productions for inductive predicates—into a term rewrite system (TRS, for short) such that a quantifier-free sequent over the first-order logic with the inductive definition set is valid if and only if its corresponding equation is an inductive theorem of the TRS. The resulting TRS is composed of three parts: Rewrite rules for logical connectives and a binary symbol for sequents; rewrite rules for productions; rewrite rules for the co-patterns of the second part. For correctness of the resulting TRS, we assume a certain property of the inductive definition set, which is a sufficient condition for ground termination and ground confluence of the resulting TRS. The transformation aims at comparing cyclic proof systems and rewriting induction.

Transforming Programs with Counting Semaphores into Logically Constrained Term Rewrite Systems

Misaki Kojima, Naoki Nishida, and Masahiko Sakai

Record of the 83rd National Convention of IPSJ page： 229 - 230 2021.3

Speeding up combinatorial optimization solver CombSQL+ by introducing Pseudo-Boolean constraints

Junichiro Kishi, Masahiko Sakai, Naoki Nishida, and Kenji Hashimoto

IEICE Technical Rerport Vol. 120 ( 343 ) page： 66-71 2021.1

Language：Japanese

The authors have proposed a solver CombSQL+ for combinatorial optimization problems (COPs) described in extended SQL language. The system generates QFLIA constraints by executing an SQL query transformed from an input description, and then solves them by an SMT solver. This report proposes an improvement of the system to generate constraints in pseudo-Boolean forms if possible. We report that the enhancement accelerates more than seven times faster for a problem.

Reversible CSP Computations Reviewed

Carlos Galindo, Naoki Nishida, Josep Silva, and Salvador Tamarit

IEEE Transactions on Parallel and Distributed Systems Vol. 32 ( 6 ) page： 1425-1436 2021.1

Language：English Publishing type：Research paper (scientific journal)

Reversibility enables a program to be executed both forwards and backwards. This ability allows programmers to backtrack the execution to a previous state. This is essential if the computation is not deterministic because re-running the program forwards may not lead to that state of interest. Reversibility of sequential programs has been well studied and a strong theoretical basis exists. Contrarily, reversibility of concurrent programs is still very young, especially in the practical side. For instance, in the particular case of the Communicating Sequential Processes (CSP) language, reversibility is practically missing. In this article, we present a new technique, including its formal definition and its implementation, to reverse CSP computations. Most of the ideas presented can be directly applied to other concurrent specification languages such as Promela or CCS, but we center the discussion and the implementation on CSP. The technique proposes different forms of reversibility, including strict reversibility and causal-consistent reversibility. On the practical side, we provide an implementation of a system to reverse CSP computations that is able to highlight the source code that is being executed in each forwards/backwards computation step, and that has been optimized to be scalable to real systems.

DOI： 10.1109/TPDS.2021.3051747

ReverCSP: Time-Travelling in CSP Computations Reviewed

Carlos Galindo, Naoki Nishida, Josep Silva, and Salvador Tamarit

Proceedings of the 12th International Conference on Reversible Computation, Lecture Notes in Computer Science Vol. 12227 page： 239-245 2020.7

Language：English

This paper presents reverCSP, a tool to animate both forward and backward CSP computations. This ability to reverse computations can be done step by step or backtracking to a given desired state of interest. reverCSP allows us to reverse computations exactly in the same order in which they happened, or also in a causally-consistent way. Therefore, reverCSP is a tool that can be especially useful to comprehend, analyze, and debug computations. reverCSP is an open-source project publicly available for the community. We describe the tool and its functionality, and we provide implementation details so that it can be reimplemented for other languages.

DOI： 10.1007/978-3-030-52482-1_14

Confluence Competition 2020 International coauthorship

Aart Middeldorp, Naoki Nishida, Kiraku Shintani, and Johannes Waldmann

Proceedings of the 9th International Workshop on Confluence page： 53 2020.6

CO3 (Version 2.1)

Naoki Nishida

Proceedings of the 9th International Workshop on Confluence page： 67 2020.6

　 PREV - NEXT 　

<NISHIDA Naoki>

Papers - NISHIDA Naoki