関数型言語MLによるプレスブルガー文真偽判定ルーチンの開発と検証支援システムへの応用  [in Japanese] An implementation of a decision procedure for Presburger sentences in ML and its application to verification support system  [in Japanese]

Access this Article

Search this Article

Author(s)

Abstract

本稿では,関数型プログラミング言語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.

Journal

  • Technical report of IEICE. SS

    Technical report of IEICE. SS 103(708), 7-12, 2004-03-08

    The Institute of Electronics, Information and Communication Engineers

References:  20

Cited by:  1

Codes

  • NII Article ID (NAID)
    110003276708
  • NII NACSIS-CAT ID (NCID)
    AN10013287
  • Text Lang
    JPN
  • Article Type
    Journal Article
  • ISSN
    09135685
  • NDL Article ID
    6926164
  • NDL Source Classification
    ZN33(科学技術--電気工学・電気機械工業--電子工学・電気通信)
  • NDL Call No.
    Z16-940
  • Data Source
    CJP  CJPref  NDL  NII-ELS  IR 
Page Top