関数型言語MLによるプレスブルガー文真偽判定ルーチンの開発と検証支援システムへの応用

才村, 徹也; 岡野, 浩三; 谷口, 健一

このアイテムのアクセス数:71件（2021-10-22 20:26 集計）

このアイテムへのリンクには次のURLをご利用ください:http://hdl.handle.net/11094/27413

閲覧可能ファイル

ファイル	フォーマット	サイズ	閲覧回数	説明
itr103_708_007	pdf	723 KB	22

論文情報

タイトル	関数型言語MLによるプレスブルガー文真偽判定ルーチンの開発と検証支援システムへの応用
別タイトル	An implementation of a decision procedure for Presburger sentences in ML and its application to verification support system
タイトル (ヨミ)	カンスウガタ　ゲンゴ　ML　ニ　ヨル　プレスブルガー　ブン　シンギ　ハンテイ　ルーチン　ノ　カイハツ　ト　ケンショウ　シエン　システム　ヘノ　オウヨウ
著者	才村, 徹也才村, 徹也
	岡野, 浩三岡野, 浩三
	谷口, 健一谷口, 健一
著者の別表記	Saimura, Tetsuya
	Okano, Kozo
	Taniguchi, Kenichi
著者 (ヨミ)	サイムラ, テツヤ
	オカノ, コウゾウ
	タニグチ, ケンイチ
キーワード等	形式的検証
	関数型プログラミング言語
	ML
	プレスブルガー文
	formal verification
	functional language
	Presburger sentences
抄録	本稿では,関数型プログラミング言語MLにより実装した整数プレイブルガー文真偽判定ルーチンについて述べる.このルーチンは一般のプレスブルガー文を入力とするが,ある限定クラスにおいては高速に動作する.研究グループで行ったCPU KUE-CHIP2の検証で用いたプレスブルガー文に対して評価実験を行い,適当な速度で真偽判定が行えることを確認した.また,作成したルーチンを用いた形式的検証支援システムについても述べる.
抄録	This paper presents an implementation of a decision procedure for Presburger sentences in functional programming language ML. It uses a fast algorithm for inputs in the from of universal quantifier prenex form; for the other inputs, its uses a general known algorithm. We have applied the procedure to verification of CPU KUE-CHIP2. The results show its effectiveness. We also describe an outline of verification support system for ML, where the decision procedure for Presburger sentences will be used as central engine of verification system.
公開者	電子情報通信学会
公開者の別表記	The Institute of Electronics, Information and Communication Engineers
公開者 (ヨミ)	デンシ　ジョウホウ　ツウシン　ガッカイ
掲載誌名	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
巻	103
号	708
開始ページ	7
終了ページ	12
刊行年月	2004-03-08
ISSN	09135685
NCID	AN10013287
URL	http://hdl.handle.net/11094/27413
権利情報	Copyright © 2004 IEICE
権利情報	本文データはCiNiiから複製したものである
言語	日本語
カテゴリ	学術雑誌論文 Journal Article

著者版フラグ	publisher
NII資源タイプ	学術雑誌論文
ローカル資源タイプ	学術雑誌論文
dcmi資源タイプ	text
DCTERMS.bibliographicCitation	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス.103(708) P.7-P.12
DC.title	関数型言語MLによるプレスブルガー文真偽判定ルーチンの開発と検証支援システムへの応用
DCTERMS.alternative	An implementation of a decision procedure for Presburger sentences in ML and its application to verification support system
DC.creator	才村, 徹也
	岡野, 浩三
	谷口, 健一
DC.creator	Saimura, Tetsuya
	Okano, Kozo
	Taniguchi, Kenichi
DC.publisher	電子情報通信学会
DC.language" scheme="DCTERMS.RFC1766	日本語
DCTERMS.issued" scheme="DCTERMS.W3CDTF	2004-03-08
DC.identifier" scheme="DCTERMS.URI	http://hdl.handle.net/11094/27413
DC.subject	形式的検証
	関数型プログラミング言語
	ML
	プレスブルガー文
	formal verification
	functional language
	Presburger sentences
DCTERMS.abstract	本稿では,関数型プログラミング言語MLにより実装した整数プレイブルガー文真偽判定ルーチンについて述べる.このルーチンは一般のプレスブルガー文を入力とするが,ある限定クラスにおいては高速に動作する.研究グループで行ったCPU KUE-CHIP2の検証で用いたプレスブルガー文に対して評価実験を行い,適当な速度で真偽判定が行えることを確認した.また,作成したルーチンを用いた形式的検証支援システムについても述べる.
DCTERMS.abstract	This paper presents an implementation of a decision procedure for Presburger sentences in functional programming language ML. It uses a fast algorithm for inputs in the from of universal quantifier prenex form; for the other inputs, its uses a general known algorithm. We have applied the procedure to verification of CPU KUE-CHIP2. The results show its effectiveness. We also describe an outline of verification support system for ML, where the decision procedure for Presburger sentences will be used as central engine of verification system.
DC.rights	Copyright © 2004 IEICE
DC.rights	本文データはCiNiiから複製したものである
citation_title	関数型言語MLによるプレスブルガー文真偽判定ルーチンの開発と検証支援システムへの応用
citation_author	才村, 徹也
	岡野, 浩三
	谷口, 健一
citation_publisher	電子情報通信学会
citation_language	日本語
citation_date	2004-03-08
citation_journal_title	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
citation_volume	103
citation_issue	708
citation_firstpage	7
citation_lastpage	12
citation_issn	09135685
citation_public_url	http://hdl.handle.net/11094/27413
citation_keywords	形式的検証
	関数型プログラミング言語
	ML
	プレスブルガー文
	formal verification
	functional language
	Presburger sentences

閲覧可能ファイル

論文情報

論文詳細を表示