Interpolant-Based Transition Relation Approximation
In predicate abstraction, exact image computation is problematic, requiring in the worst case an exponential number of calls to a decision procedure. For this reason, software model checkers typically use a weak approximation of the image. This can result in a failure to prove a property, even given...
| 主要な著者: | , |
|---|---|
| フォーマット: | 論文 |
| 言語: | English |
| 出版事項: |
Logical Methods in Computer Science e.V.
2007-11-01
|
| シリーズ: | Logical Methods in Computer Science |
| 主題: | |
| オンライン･アクセス: | https://lmcs.episciences.org/1152/pdf |