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...
第一著者: | Kroening, D |
---|---|
フォーマット: | Journal article |
出版事項: |
Elsevier
2006
|
類似資料
-
Computing Over−Approximations with Bounded Model Checking
著者:: Kroening, D
出版事項: (2006) -
Computational challenges in bounded model checking
著者:: Clarke, E, 等
出版事項: (2005) -
Computational challenges in bounded model checking.
著者:: Clarke, E, 等
出版事項: (2005) -
Computational Challenges in Bounded Model Checking
著者:: Clarke, E, 等
出版事項: (2015) -
Completeness and Complexity of Bounded Model Checking
著者:: Clarke, E, 等
出版事項: (2004)