Efficient verification of concurrent systems using synchronisation analysis and SAT/SMT solving
This article investigates how the use of approximations can make the formal verification of concurrent systems scalable. We propose the idea of synchronisation analysis to automatically capture global invariants and approximate reachability. We calculate invariants on how components participate on g...
| Main Authors: | , , |
|---|---|
| Format: | Journal article |
| Published: |
Association for Computing Machinery
2019
|