研究者詳細 - 西田　直樹

論文 - 西田　直樹

分割表示 254 件中 21 - 40 件目／全件表示 >>

Naoki Nishida, Misaki Kojima, and Ayuka Matsumi

Proceedings of the 12th International Workshop on Confluence 頁： 67 2023年8月

A New Format for Rewrite Systems 査読有り国際共著

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 頁： 32 - 37 2023年8月

Confluence Competition 2023 国際共著

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

Proceedings of the 12th International Workshop on Confluence 頁： 61 - 62 2023年8月

On Representations of Waiting Queues for Semaphores in Logically Constrained Term Rewrite Systems 査読有り

Misaki Kojima and Naoki Nishida

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

担当区分：最終著者,　責任著者記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）

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 査読有り

Naoki Nishida, Misaki Kojima, and Ayuka Matsumi

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

担当区分：最終著者,　責任著者記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）

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.

ビットベクトル制約付き項書換え系の停止性証明のための多項式解釈プロセッサについて

松見歩佳，西田直樹，小嶋美咲，申東訓

電子情報通信学会技術報告 122 巻 ( 432 ) 頁： 85 - 90 2023年3月

担当区分：責任著者記述言語：日本語掲載種別：研究論文（研究会，シンポジウム資料等）

ビットベクトル制約付き項書換え系（BV-LCTRS）はC言語などのプログラムのモデルとして有用である．等価性検証に書換え帰納法を用いる際には，与えられた書換え系に帰納法の仮定となる書換え規則を加えて得られる書換え系の停止性が何度も証明される. LCTRSの停止性証明には項書換え系と同様に依存対プロセッサを使用して証明する枠組みの依存対フレームワークが用いられるが，整数制約を持つLCTRSの停止性証明において最も強力なプロセッサの1つである多項式解釈プロセッサはBV-LCTRSには適用できない．本稿では，BV-LCTRSの停止性証明を強化することを目的として，新たな依存対プロセッサとしてビットベクトル上の多項式解釈プロセッサと単一自己ループ除去プロセッサを提案する．

From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting 査読有り国際誌

Misaki Kojima and Naoki Nishida

Proceedings of the 25th International Symposium on Practical Aspects of Declarative Languages, Lecture Notes in Computer Science 13880 巻頁： 161 - 179 2023年1月

担当区分：最終著者,　責任著者記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）出版者・発行元：Springer, Cham

An all-path reachability problem of a logically constrained term rewrite system is a pair of constrained terms representing state sets, and is demonically valid if every finite execution path from any state in the first set to a terminating 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 a logically constrained term rewrite system to an all-path reachability problem of the system. In this paper, we extend the framework to verification of starvation freedom of asynchronous integer transition systems with shared variables such that some processes enter critical sections.

DOI： 10.1007/978-3-031-24841-2_11

CO3 (Version 2.3)

Naoki Nishida and Misaki Kojima

Proceedings of the 11th International Workshop on Confluence 頁： 63 2022年8月

Confluence Competition 2022 国際共著

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

Proceedings of the 11th International Workshop on Confluence 頁： 54 2022年8月

On Transforming Imperative Programs into Logically Constrained Term Rewrite Systems via Injective Functions from Configurations to Terms 査読有り

Naoki Nishida, Misaki Kojima, and Takumi Kato

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

担当区分：筆頭著者,　責任著者記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）

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 査読有り

Misaki Kojima and Naoki Nishida

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

担当区分：最終著者,　責任著者記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）

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 査読有り

Shujun Zhang and Naoki Nishida

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

担当区分：最終著者,　責任著者記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）

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 査読有り国際誌 Open Access

Shujun Zhang and Naoki Nishida

Journal of Logical and Algebraic Methods in Programming 127 巻頁： 1 - 17 2022年6月

担当区分：最終著者,　責任著者記述言語：英語掲載種別：研究論文（学術雑誌）

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

Open Access

On Transforming Cut- and Quantifier-Free Cyclic Proofs into Rewriting-Induction Proofs 査読有り国際誌

Shujun Zhang and Naoki Nishida

Proceedings of the 16th International Symposium on Functional and Logic Programming (FLOPS 2022), Lecture Notes in Computer Science 13215 巻頁： 262 - 281 2022年5月

担当区分：責任著者記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）出版者・発行元：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

プログラム逆化のための文脈自由表現の等価関係に基づく項書換え系決定化手法の実装 Open Access

熊谷妃美香，西田直樹

情報処理学会第84回全国大会講演論文集頁： 271 - 272 2022年3月

LLVM中間表現の意味論規則を表現する制約付き書換え規則について

加藤拓洋，西田直樹，酒井正彦

電子情報通信学会技術報告 121 巻 ( 318 ) 頁： 89 - 94 2022年1月

担当区分：責任著者記述言語：日本語掲載種別：研究論文（研究会，シンポジウム資料等）

C言語に沿った簡易プログラミング言語を論理制約付き項書換え系（LCTRS）に変換し，元のプログラムの性質をLCTRSの性質に帰着して検証する手法が研究されている．本稿では，LCTRSへ変換できるプログラミング言語を増やすことをめざし，LLVM中間表現からLCTRSへの変換を提案する．一般に，LLVM中間表現の意味論ではメモリ及び変数への割当てが写像として計算状態に含まれる．一方，写像をデータとして扱わないLCTRSへの既存の変換では写像の値域を関数記号の引数として保持させることになり正当性証明を複雑にする．本稿ではメモリ及び割当てに相当する写像をデータとして扱うLCTRSを用いることで，変換とその正当性証明を簡潔にする．具体的には，プログラムの計算状態から項への単射関数を定義し，LLVM中間表現の各命令とそれに適用可能な各意味論規則に対して，1つの制約付き書換え規則を生成する．

制約付き書換え帰納法におけるラグランジュ補間を用いた補題生成

比嘉慎哉，西田直樹，酒井正彦

日本ソフトウェア科学会第38回大会講演論文集頁： 1 - 13 2021年9月

Determinization of inverted grammar programs via context-free expressions 査読有り国際誌 Open Access

Naoki Nishida and Minami Niwa

Journal of Logical and Algebraic Methods in Programming 122 巻頁： 1 - 26 2021年8月

担当区分：筆頭著者,　責任著者記述言語：英語掲載種別：研究論文（学術雑誌）

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

Open Access

その他リンク： http://hdl.handle.net/2237/0002001914

Confluence Competition 2021 国際共著

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

Proceedings of the 10th International Workshop on Confluence 頁： 51 2021年7月

CO3 (Version 2.2)

Naoki Nishida

Proceedings of the 10th International Workshop on Confluence 頁： 61 2021年7月