研究者詳細 - 西田　直樹

講演・口頭発表等 - 西田　直樹

分割表示 >> ／全件表示 49 件中 1 - 49 件目

論理制約付き項書き換えシステムにおける制約付き最汎書き換え国際共著

高畑幹汰，Jonas Schöpf，西田直樹，青戸等人

第27回プログラミングおよびプログラミング言語ワークショップ（PPL 2025） 2025年3月日本ソフトウェア科学会プログラミング論研究会

All-Path Reachability for Starvation Freedom Under Process Fairness

Naoki Nishida

the 60th TRS Meeting 2024年10月7日

A Sufficient Condition of Logically Constrained Term Rewrite Systems for Decidability of All-Path Reachability Problems with Constant Destinations

Misaki Kojima and Naoki Nishida

th 146th Workshop on IPSJ Special Interest Group on Programming 2023年10月31日 IPSJ Special Interest Group on Programming

On Constrained Narrowing of Logically Constrained Term Rewrite Systems

Naoki Nishida

the 59th TRS Meeting 2023年9月28日

Unravelings and Narrowing Trees Towards Confluence of Deterministic CTRSs 招待有り国際会議

Naoki Nishida

12th International Workshop on Confluence 2023年8月23日 Cyrille Chenavier and Sarah Winkler

On Transforming Imperative Programs into LCTRSs via Injective Functions from Configurations to Terms

Naoki Nishida

the 57th TRS Meeting 2022年9月28日

Inversion and Determinization in Term Rewriting 招待有り国際会議

Naoki Nishida

the meeting of IFIP Working Group 1.6: Rewriting 2022年7月31日 IFIP Working Group 1.6: Rewriting

開催年月日： 2022年7月

記述言語：英語会議種別：口頭発表（一般）

開催地：Haifa, Israel 国名：イスラエル国

As a transformational approach, inversion is formulated in several settings, and the basic ideas are naive and similar. To generate a better form, e.g., non-overlapping systems if possible, determinization is used as a post-process of inversion for injective functions, and is the most challenging part in developing an inversion framework. In this talk, I introduce a framework of inversion and determinization in term rewriting. First, I explain a direct inversion of deterministic CTRSs, and a direct MSV-based determinization. Next, I explain the framework proposed by Gluck and Kawabe, which uses context-free grammars as intermediate representations of CTRSs. Finally, I explain a framework based on context-free expressions.

On Semantically Equivalent Operations for Inversion of DCTRSs

Naoki Nishida

the 56th TRS Meeting 2022年2月24日

On Improving Confluence and Infeasibility Proofs in CO3

Naoki Nishida

the 55th TRS Meeting 2021年9月29日

Transformation of Concurrent Programs with Semaphores into LCTRSs

Naoki Nishida

the 54th TRS Meeting 2021年3月16日

Proving Infeasibility by Basic Narrowing

Naoki Nishida

the 50th TRS Meeting

Proving Infeasibility by Narrowing Trees

Naoki Nishida

the 49th TRS Meeting

組合せ最適化問題を記述するための関係代数の集合上への拡張

坂梨元軌，酒井正彦，西田直樹，橋本健二

第20回プログラミングおよびプログラミング言語ワークショップ

開催年月日： 2018年3月

記述言語：日本語会議種別：ポスター発表

開催地：皆生グランドホテル天水国名：日本国

組合せ最適化問題は様々な分野に応用できるが，効率良く解くためには専門知識を必要とするという問題がある．本研究では，組合せ最適化問題を簡潔に記述できなおかつ効率的に解くことができるシステムの構築を目指して，理論的な枠組として関係の集合上に拡張した関係代数を提案し，それに基づく拡張SQL構文とその汎用ソルバによる解法を議論する．

配列を含むC言語サブセットから難解言語Malbolgeへのコンパイラ

岩金カナン，坂梨元軌，酒井正彦，西田直樹，橋本健二

第20回プログラミングおよびプログラミング言語ワークショップ

開催年月日： 2018年3月

記述言語：日本語会議種別：ポスター発表

開催地：皆生グランドホテル天水国名：日本国

難解プログラミング言語とは意図的に読解が困難になるように設計された言語であり、中でも難解な言語としてMalbolgeがある。現在では低級アセンブリ言語と制御付き疑似命令列を経てC言語に制限を設けた高級言語からのコンパイラが実現されている。しかしこの高級言語では配列を扱うことができず、複雑なプログラムが書けなかった。本研究では配列を含む高級言語を処理してMalbolgeへ変換する手法を実装した。この変換にはメモリの空き領域をスタックとして用いることで実現した。

From Dependency Chains to Bounded Monotone Sequences of Integers

Naoki Nishida

the 47th TRS Meeting

On Proving Infeasibility of Conditional Critical Pairs via Narrowing Trees

Naoki Nishida

the 46th TRS Meeting

Heuristics for Proving Termination of Constrained Rewriting Systems via Rule Duplication 国際会議

Naoki Nishida

4th Austria - Japan Summer Workshop on Term Rewriting

On Uninterpreted Functions in Proving Termination of Constrained Rewriting

Naoki Nishida

the 41st TRS Meeting

On Soundness for Reduction of TRSs Obtained by Condition Elimination for Normal CTRSs

Naoki Nishida

the 40th TRS Meeting

A Finite Representation of the Narrowing Space and its Application 国際会議

Naoki Nishida

COMPUTER SCIENCE COLLOQUIUM, IMADA, University of Southern Denmark

Automated Verification of C Programs via Rewriting Induction of Constrained TRSs 国際会議

Naoki Nishida

Seminar at Research Group "Verification meets Algorithm Engineering", the Institute for Theoretical Computer Science, Karlsruhe Institute of Technology

開催年月日： 2013年7月

記述言語：英語会議種別：口頭発表（招待・特別）

国名：ドイツ連邦共和国

In this talk, we introduce an automated theorem proving method based on rewriting induction of constrained TRSs, and show how to apply it to the verification of C programs over integers. Especially, we show a technique to automatically generate (a candidate of) lamma equations that are necessary for the proof.

Computing More Specific Versions of Conditional Rewriting Systems

Naoki Nishida

the 37th TRS Meeting

Program Inversion and MSV Transformation in Term Rewriting 国際会議

Naoki Nishida

Master Seminar 1, Institute of Computer Science, University of Innsbruck

開催年月日： 2012年10月

記述言語：英語会議種別：口頭発表（一般）

国名：オーストリア共和国

In this talk, I present two principles of program inversion
in term rewriting setting, a classical one and another one for tail
recursion. Rewrite rules generated by inversion methods based on the
principles are often non-deterministic w.r.t. application of rules to
redexes even if given functions are injective. For this reason,
determinization of inverted programs is one of the most challenging
topics in program inversion of injective functions. To make inverted
programs deterministic, I present an MSV transformation of term
rewriting systems, which converts a rewrite system to a more specific
version. The notion of MSV originated from the context of logic
programs.

Program Inversion for Tail Recursive Functions 国際会議

Naoki Nishida

Seminar at DSIC, Technical University of Valencia

多重文脈書換え帰納法における反証と補題追加

坂田翼, 西田直樹, 酒井正彦, 草刈圭一朗, 坂部俊樹

日本ソフトウェア科学会第28回大会

On Soundness of CTRS Transformations

Naoki Nishida

the 35th TRS Meeting

On Verifying Equivalence between Functions in Constrained TRSs via Tree Homomorphisms

Naoki Nishida

the 35th TRS Meeting

難解言語Malbolgeにおける高級アセンブリ言語への加算命令の追加

安藤聡, 長坂哲, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹

第13回プログラミングおよびプログラミング言語ワークショップ

制約付き項書換え系における木準同型写像を用いた等価性検証ツール

高桑一也, 西田直樹, 大場康司, 酒井正彦, 坂部俊樹, 草刈圭一朗

第13回プログラミングおよびプログラミング言語ワークショップ

難解言語Malbolgeにおけるプログラミング環境の構築と改良

長坂哲, 安藤聡, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹

第13回プログラミングおよびプログラミング言語ワークショップ

On Inverting Tail Recursive Functions

Naoki Nishida

the 34th TRS Meeting

例外処理を持つ関数型プログラムの停止性証明法

馬場正貴, 酒井正彦, 濱口毅, 西田直樹, 坂部俊樹, 草刈圭一朗

第12回プログラミングおよびプログラミング言語ワークショップ

SATソルバを利用したお絵かきロジックの問題作成支援ツール

長坂哲, 伊藤寛之, 酒井正彦, 草刈圭一朗, 西田直樹, 坂部俊樹

組合せゲーム・パズルミニプロジェクト第5回ミニ研究集会

On Improving Lemma Generation Framework for Constrained Term Rewriting Systems

the 33rd TRS Meeting

On Automating Theorem Proving for Constrained Equations

the 32nd TRS Meeting

制約付き等式の定理自動証明器の試作

西田直樹, 中林直生, 酒井正彦, 草刈圭一朗, 坂部俊樹

日本ソフトウェア科学会第26回大会

潜在帰納法を利用した手続き型プログラム検証の試み

古市祐樹, 西田直樹, 酒井正彦 , 草刈圭一朗, 坂部俊樹

第68回情報処理学会・プログラミング研究会

Comparison of Unraveling Techniques for Deterministic Conditional Term Rewriting Systems 国際会議

2nd Austria - Japan Summer Workshop on Term Rewriting

Convergent Term Rewriting Systems for Computing Inverses of Injective Functions

the 28th TRS Meeting

On Reachability of Oriented Conditional Term Rewriting Systems

the 27th TRS Meeting

Improving Unraveling for Deterministic Conditional Term Rewriting Systems

the 26th TRS Meeting

Dependency Graph Method for Proving Termination of Narrowing 国際会議

Austria - Japan Summer Workshop on Term Rewriting

Partial Inversion of Constructor Term Rewriting Systems

the 25th TRS Meeting

Transformational Approach to Inverse Computation in Term Rewriting

the 18th Tokyo Programming Seminar (ToPS)

Completeness of Unraveling Transformation for Left-Linear Conditional Term Rewriting Systems

the 24th TRS Meeting

Basic Narrowing Improves Efficiency of Computation of Right-Linear Term Rewriting Systems with Extra Variables

the 23rd TRS Meeting

Condition for Generation of Terminating Inverse TRSs from Constructor TRSs

the 22nd TRS Meeting

Narrowing-Based Reduction of Term Rewriting Systems with Extra Variables

the 21st TRS Meeting

On Generating Inverse Systems of Constructor TRSs

the 20th TRS Meeting

　前のページ - 次のページ　

<西田 直樹>

講演・口頭発表等 - 西田 直樹

<西田　直樹>

講演・口頭発表等 - 西田　直樹