Methods for using Agda to prove Safety and Liveness for Concurrent Programs

Examensarbete för kandidatexamen

Please use this identifier to cite or link to this item:
Download file(s):
File Description SizeFormat 
251204.pdfFulltext655.01 kBAdobe PDFView/Open
Type: Examensarbete för kandidatexamen
Bachelor Thesis
Title: Methods for using Agda to prove Safety and Liveness for Concurrent Programs
Authors: Bergsten, Erik
Larsson, Oskar
Rastemo, Tobias
Rutqvist, Oskar
Standar, Anderas
Abstract: It is hard and error-prone to prove that a given concurrent program has a given property. To help develop such proofs, a modern implementation of dependent type theory, the proof checking tool Agda [Nor09], is used. The methods are based on the semi-formal theory of the semantics of concurrent programming from [OL82] (Owicki and Lamport, 1981);. The formalisation and implementation in Agda is done with two di erent approaches, which we call Proof by Construction and Proof by Control Flow. The rst uses the dependent data types of Agda to create proofs in the form of type elements. The second uses recursive functions to check proofs written down as a tree of steps. With each method, how to prove liveness properties for concurrent programs is shown. For safety properties, time constraints restricted the work to proofs for sequential programs. The Agda implementations of these methods work well, but like formal and manually constructed proofs our machine checked proofs are still long and tedious. The implementations have potential for further development.
Keywords: Data- och informationsvetenskap;Computer and Information Science
Issue Date: 2017
Publisher: Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers)
Collection:Examensarbeten för kandidatexamen // Bachelor Theses

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