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...
Главные авторы: | Groce, A, Kroening, D |
---|---|
Формат: | Journal article |
Опубликовано: |
Elsevier
2005
|
Схожие документы
The Breakdown Point — Examples and Counterexamples
по: P.L. Davies, и др.
Опубликовано: (2007-03-01)
по: P.L. Davies, и др.
Опубликовано: (2007-03-01)
Схожие документы
-
Making the Most of BMC Counterexamples
по: Groce, A, и др.
Опубликовано: (2005) -
Understanding Counterexamples with explain
по: Groce, A, и др.
Опубликовано: (2004) -
Counterexample Guided Abstraction Refinement via Program Execution
по: Groce, A, и др.
Опубликовано: (2004) -
Counterexample−guided Precondition Inference
по: Seghir, M, и др.
Опубликовано: (2013) -
Counterexample-guided precondition inference
по: Seghir, M, и др.
Опубликовано: (2013)