Approximation Refinement for Interpolation−Based Model Checking

Model checking using Craig interpolants provides an effective method for computing an over-approximation of the set of reachable states using a SAT solver. This method requires proofs of unsatisfiability from the SAT solver to progress. If an over-approximation leads to a satisfiable formula, the co...

Mô tả đầy đủ

Chi tiết về thư mục
Những tác giả chính: D'Silva, V, Purandare, M, Kroening, D
Tác giả khác: Logozzo, F
Định dạng: Conference item
Được phát hành: Springer 2008