K-induction-based model checking of concurrent systems with unbounded integer variables

ジョウカイ　ノ　ナイ　セイスウガタ　ヘンスウ　ヲ　ユウスル　ヘイコウ　システム　ニ　タイスル　kキノウホウ　ヲ　モチイタ　モデル　ケンサ

イノウエ, ヒロユキ

Inoue, Hiroyuki

土屋, 達弘

ツチヤ, タツヒロ

Tsuchiya, Tatsuhiro

菊野, 亨

キクノ, トオル

Kikuno, Tohru

The Institute of Electronics, Information and Communication Engineers

デンシ　ジョウホウ　ツウシン　ガッカイ

k帰納法

SMT

並行システム

model checking

k-induction

concurrent systems

We discuss k-induction-based model checking that uses a Satisfiability Modulo Theories (SMT) solver. The state space of a system with unbounded integer variables is infinite; thus it is impossible to visit all of its states. K-induction is one of the model checking approaches that can be used to reason about such an infinite state space. In this approach, the problem of model checking is reduced to the satisfiability problem that can be solved by an SMT solver. However, this approach does not work effectively when applied to concurrent programs, because the formula representing the behaviors of systems with high concurrency tends to become very large. To overcome this problem, we propose an alternative approach that uses more compact formulas.

本文データはCiNiiから複製したものである

土屋, 達弘

菊野, 亨