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: | Antonino, P, Gibson-Robinaon, T, Roscoe, A |
---|---|
Format: | Journal article |
Published: |
Association for Computing Machinery
2019
|
Similar Items
-
Efficient verification of comcurrent systems using local analysis based approximations and SAT solving
by: Antonino, P, et al.
Published: (2019) -
SAT and SMT-Based Verification of Security Protocols Including Time Aspects
by: Sabina Szymoniak, et al.
Published: (2021-04-01) -
On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency
by: Horn, A, et al.
Published: (2015) -
On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency
by: Horn, A, et al.
Published: (2015) -
Logic for concurrency and synchronisation /
by: Queiroz, Ruy J.G.B. de
Published: (2003)