Skip navigation
Skip navigation

Verification of Concurrent Data Structures with TLA

Cai, Zixian

Description

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)
URI: http://hdl.handle.net/1885/151830

Download

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:  22 January 2019/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator