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...
| Հիմնական հեղինակ: | |
|---|---|
| Ձևաչափ: | Journal article |
| Հրապարակվել է: |
Elsevier
2006
|