Counterexample-guided abstraction refinement for symmetric concurrent programs
Predicate abstraction and counterexample-guided abstraction refinement (CEGAR) have enabled finite-state model checking of software written in mainstream programming languages. This combination of techniques has been successful in analysing system-level sequential C code. In contrast, there is littl...
| Hauptverfasser: | , , |
|---|---|
| Format: | Journal article |
| Veröffentlicht: |
Springer
2012
|