千代 英一郎

近年，SMTソルバの研究がさかんに行われてきており，様々な制約問題を解けるよう飛躍的に進歩している．しかしながら，SMTソルバは線形制約式の解を短時間で求められることが多いのに対し，高次の制約式の解を求めるのに時間がかかってしまうことがある．たとえば，代表的なプログラム検査であるループ停止性検査等で必要となる複雑な制約式の場合，検査に数日を要することもあり，実用上の課題となっている．この問題に対して，本発表では，変数のとりうる値域を限定した検査を，値域を変えて繰り返すことで，制約式の充足可能性を推定する方法について報告する．それぞれの試行を短い時間で打ち切ることにより，結果が得られないことを避けることができる．In recent years, studies of SMT solvers are conducted flourishingly and progress drastically to be able to solve various constraint satisfaction problems. However, while the SMT solver tends to find solution of linear constraints efficiently, it may take a few days to find solutions of the higher degree constraints needed for checking loop termination. For this problem, we examine methods to estimate the satisfiability of constraints by iterative checking (trial) with range restriction of variables. In this presentation, we report some experimental results about trial.