Making the most of BMC counterexamples

The value of model checking counterexamples for debugging programs (and specifications) is widely recognized. Unfortunately, bounded model checkers often produce counterexamples that are difficult to understand due to the values chosen by a SAT solver. This paper presents two approaches to making be...

Mô tả đầy đủ

Chi tiết về thư mục
Những tác giả chính: Groce, A, Kroening, D
Định dạng: Journal article
Được phát hành: Elsevier 2005