Verification of Concurrent Data Structures with TLA
Concurrent systems have critical applications such as aviation. Due to their inherent complexity, mechanised verification is well suited for reasoning about the safety and liveness properties of such systems. Temporal logics, such as TLA and LTL, have been used to verify distributed systems and protocols. However, it is not clear whether these logics are good fits for modelling and verifying concurrent data structures. This work describes how Temporal Logic of Actions (TLA) can be adapted to...[Show more]
|Collections||ANU Research Publications|
|Type:||Report (Student work)|
|20181109-SCNC2102-Zixian.pdf||Report||411.75 kB||Adobe PDF|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.