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

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

電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス, 2004, 103(708), 7-12

アクセス数:523件（2025-11-06 18:50 集計）

固定URL: https://hdl.handle.net/11094/27413

閲覧可能ファイル 

ファイル フォーマット 利用条件 サイズ 閲覧回数 利用開始日 説明 information
itr103_708_007 pdf なし 723 KB 76 2014.04.11  

論文情報

ファイル出力 EndNote Basic出力 Mendeley出力

タイトル
関数型言語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
PISSN
09135685
NCID
AN10013287
アクセス権
open access
権利情報
Copyright © 2004 IEICE
本文データはCiNiiから複製したものである
出版タイプ
Version of Record
カテゴリ
学術雑誌論文 Journal Article