首页    期刊浏览 2024年11月29日 星期五
登录注册

文章基本信息

  • 标题:高速なMCS列挙を利用した準最弱事前条件推定の改良
  • 本地全文:下载
  • 作者:今井 健男 ; 酒井 政裕 ; 萩谷 昌己
  • 期刊名称:コンピュータ ソフトウェア
  • 印刷版ISSN:0289-6540
  • 出版年度:2015
  • 卷号:32
  • 期号:4
  • 页码:4_161-4_175
  • DOI:10.11309/jssst.32.4_161
  • 出版社:Japan Society for Software Science and Technology
  • 摘要:

    我々は以前,制約ソルバを用いて,自動生成した述語の組み合わせからなるプログラムの事前条件で最弱なもの(準最弱事前条件)を推定する手法を提案した.これにはminimal unsatisfiable core(MUC)の列挙を利用していたが,計算コストが高いことが主な課題であった.MUCの列挙はminimal correction subset (MCS)の列挙を介して実現できるが,MUCの列挙が高コストである要因の1つは,このMCS列挙の高コスト性にある.我々は,本手法を通じて得られるMCSが (1) サイズを一定値に設定できる (2) MUCの一部を先に求めておくことで列挙を効率化できる,の2性質を持つことに着目し,それら性質を活かした高速化アルゴリズムを3種類提案する.3アルゴリズムそれぞれについて性能評価を行ったところ,いずれも既存手法と比較して速度向上が確認でき,MUC列挙にかかる速度比は最大10.7倍程度であった.本論文ではその結果を報告し,また各アルゴリズムの得失について考察する.

国家哲学社会科学文献中心版权所有