Skip navigation
Skip navigation

Verification of Concurrent Data Structures with TLA

Cai, Zixian


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]

CollectionsANU Research Publications
Date published: 2018-11
Type: Report (Student work)
Access Rights: Open Access


File Description SizeFormat Image
20181109-SCNC2102-Zixian.pdfReport411.75 kBAdobe PDFThumbnail

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator