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

閲覧可能ファイル 

ファイル	フォーマット	サイズ	閲覧回数	利用開始日	説明
itr103_708_007	pdf	723 KB	24	2014.04.11

論文情報

タイトル	関数型言語MLによるプレスブルガー文真偽判定ルーチンの開発と検証支援システムへの応用
	An implementation of a decision procedure for Presburger sentences in ML and its application to verification support system
	カンスウガタ　ゲンゴ　ML　ニ　ヨル　プレスブルガー　ブン　シンギ　ハンテイ　ルーチン　ノ　カイハツ　ト　ケンショウ　シエン　システム　ヘノ　オウヨウ
著者	著者名 才村, 徹也 サイムラ, テツヤ Saimura, Tetsuya
	NRID 1000070252632 1000070252632 著者名 岡野, 浩三 オカノ, コウゾウ Okano, Kozo
	NRID 1000000029513 1000000029513 著者名 谷口, 健一 タニグチ, ケンイチ 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
言語	日本語
ハンドルURL	https://hdl.handle.net/11094/27413
ISSN	09135685
NCID	AN10013287
アクセス権	open access
権利情報	Copyright © 2004 IEICE
	本文データはCiNiiから複製したものである
出版タイプ	Version of Record
カテゴリ	学術雑誌論文 Journal Article

ホームへ戻る