Methods for using Agda to prove Safety and Liveness for Concurrent Programs
Ladda ner
Typ
Examensarbete för kandidatexamen
Bachelor Thesis
Bachelor Thesis
Program
Software Engineering (300 hp)
Publicerad
2017
Författare
Bergsten, Erik
Larsson, Oskar
Rastemo, Tobias
Rutqvist, Oskar
Standar, Anderas
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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.
Beskrivning
Ämne/nyckelord
Data- och informationsvetenskap , Computer and Information Science