| 大会名称 |
|---|
| 2015年 情報科学技術フォーラム(FIT) |
| 大会コ－ド |
| F |
| 開催年 |
| 2015 |
| 発行日 |
| 2015/08/25 |
| セッション番号 |
| 1A |
| セッション名 |
| プログラミング |
| 講演日 |
| 2015/09/15 |
| 講演場所(会議室等) |
| 講義棟2階 講23 |
| 講演番号 |
| A-001 |
| タイトル |
| 変数値域限定による充足可能性判定効率化手法の検討 |
| 著者名 |
| 中山寛己, 千代英一郎, |
| キーワード |
| 抄録 |
| 充足可能性判定問題とは, 論理式が真となるような変数への値の割りてが存在するかどうかを判定する問題である. プログラム検査において，様々な検査問題を充足可能性判定問題に帰着して解く方法が知られているが，ループ停止性検査等で必要となる複雑な論理式の場合，判定に数日を要することもあり，実用上の課題となっている．本発表では，論理式中の変数の値域を限定することで1度の検査にかかる時間を減らし, 繰り返し検査することで論理式を満たす値を推定する方法について検討を行った結果にいて報告する．提案手法で課題となるのが，1度に検査する範囲を狭めることで検査にかかる時間は短くなるが， 論理式を満たす値を見つけにくくなるというトレードオフである．予備評価の結果, いくつかの論理式に対して, トレードオフの適切な解消点を得ることができた |
| 本文pdf |
| PDF download (172.7KB) |