研究者詳細 - 西田　直樹

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

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

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

　前のページ - 次のページ　

<西田 直樹>

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

<西田　直樹>

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