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...
| Autores principales: | , , |
|---|---|
| Formato: | Journal article |
| Publicado: |
Springer
2012
|