Computing over-approximations with bounded model checking

Bounded Model Checking (BMC) searches for counterexamples to a property ϕ with a bounded length k. If no such counterexample is found, k is increased. This process terminates when k exceeds the completeness threshold (i.e., k is sufficiently large to ensure that no counterexample exists) or when th...

Olles dieđut

Bibliográfalaš dieđut
Váldodahkki: Kroening, D
Materiálatiipa: Journal article
Almmustuhtton: Elsevier 2006