| Budget Amount *help |
¥20,150,000 (Direct Cost: ¥15,500,000、Indirect Cost: ¥4,650,000)
Fiscal Year 2014: ¥4,940,000 (Direct Cost: ¥3,800,000、Indirect Cost: ¥1,140,000)
Fiscal Year 2013: ¥4,940,000 (Direct Cost: ¥3,800,000、Indirect Cost: ¥1,140,000)
Fiscal Year 2012: ¥4,940,000 (Direct Cost: ¥3,800,000、Indirect Cost: ¥1,140,000)
Fiscal Year 2011: ¥5,330,000 (Direct Cost: ¥4,100,000、Indirect Cost: ¥1,230,000)
|
|---|
| Outline of Final Research Achievements |
This research extends the interval constraint propagation to the raSAT loop, which is implemented as an SMT solver raSAT. A polynomial constraint solving concludes either SAT (satisfiable) or UNSAT (unsatisfiable). raSAT is designed to intend the former, which is often used for error detection, where the latter is used for loop invariant generation. In practice, when tackling a larger problem with several hundred variables, UNSAT is detected only with the discovery of a small UNSAT core, whereas SAT is detected by finding an instance that satisfies all constraints, and often becomes a harder problem. In experiments, we newly found that several unsolved problems in SMTlib benchmark are SAT.
|
