研究者詳細 - 西田　直樹

論文 - 西田　直樹

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

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

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

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

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

熊谷妃美香，西田直樹

情報処理学会第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 査読有り国際誌

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

その他リンク： 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月

On Transforming Inductive Definition Sets into Term Rewrite Systems 査読有り

Shujun Zhang and Naoki Nishida

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

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

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.

計数セマフォを含むプログラムから論理制約付き項書換え系への変換

小嶋美咲，西田直樹，酒井正彦

情報処理学会第83回全国大会講演論文集頁： 229 - 230 2021年3月

擬ブール制約の導入による組合せ最適化ソルバCombSQL+の高速化

岸潤一郎，酒井正彦，西田直樹，橋本健二

電子情報通信学会技術報告 120 巻 ( 343 ) 頁： 66-71 2021年1月

記述言語：日本語

著者らはこれまでに，拡張したSQLで組合せ最適化問題を簡単に記述でき，かつ効率的に解くことのできる求解系CombSQL+を提案した．CombSQL+はシステム内部で，入力のSQL式からプログラム変換によって得られるSQL式をDBエンジンで実行することでいくつかの線形整数制約（QFLIA）を生成し，SMTソルバを利用してそれらの解を求めている．本稿では，変換後のSQL式で用いられる制約生成関数を工夫することで，擬ブール制約として表現できる制約を直接，擬ブール制約として生成する方法を提案する．この改良により問題によっては7倍以上の高速化が達成できたことを報告する．

Reversible CSP Computations 査読有り

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

IEEE Transactions on Parallel and Distributed Systems 32 巻 ( 6 ) 頁： 1425-1436 2021年1月

記述言語：英語掲載種別：研究論文（学術雑誌）

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

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

Proceedings of the 12th International Conference on Reversible Computation, Lecture Notes in Computer Science 12227 巻頁： 239-245 2020年7月

記述言語：英語

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 国際共著

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

Proceedings of the 9th International Workshop on Confluence 頁： 53 2020年6月

CO3 (Version 2.1)

Naoki Nishida

Proceedings of the 9th International Workshop on Confluence 頁： 67 2020年6月

Transforming Concurrent Programs with Semaphores into Logically Constrained Term Rewrite Systems 査読有り

Misaki Kojima, Naoki Nishida, and Yutaka Matsubara

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

A Case Study for Reversible Computing: Reversible Debugging of Concurrent Programs 査読有り

James Hoey, Ivan Lanese, Naoki Nishida, Irek Ulidowski, and German Vidal

Reversible Computation: Extending Horizons of Computing, Lecture Notes in Computer Science 12070 巻頁： 108-127 2020年5月

記述言語：英語掲載種別：研究論文（学術雑誌）

Reversible computing allows one to run programs not only in the usual forward direction, but also backward. A main application area for reversible computing is debugging, where one can use reversibility to go backward from a visible misbehaviour towards the bug causing it. While reversible debugging of sequential systems is well understood, reversible debugging of concurrent and distributed systems is less settled. We present here two approaches for debugging concurrent programs, one based on backtracking, which undoes actions in reverse order of execution, and one based on causal consistency, which allows one to undo any action provided that its consequences, if any, are undone beforehand. The first approach tackles an imperative language with shared memory, while the second one considers a core of the functional message-passing language Erlang. Both the approaches are based on solid formal foundations.

DOI： 10.1007/978-3-030-47361-7_5

　前のページ - 次のページ　

<西田 直樹>

論文 - 西田 直樹

<西田　直樹>

論文 - 西田　直樹