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

Visa enkel post
dc.contributor.authorBergsten, Erik
dc.contributor.authorLarsson, Oskar
dc.contributor.authorRastemo, Tobias
dc.contributor.authorRutqvist, Oskar
dc.contributor.authorStandar, Anderas
dc.contributor.departmentChalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)sv
dc.contributor.departmentChalmers University of Technology / Department of Computer Science and Engineering (Chalmers)en
dc.date.accessioned2019-07-03T14:35:02Z
dc.date.available2019-07-03T14:35:02Z
dc.date.issued2017
dc.description.abstractIt 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.
dc.identifier.urihttps://hdl.handle.net/20.500.12380/251204
dc.language.isoeng
dc.setspec.uppsokTechnology
dc.subjectData- och informationsvetenskap
dc.subjectComputer and Information Science
dc.titleMethods for using Agda to prove Safety and Liveness for Concurrent Programs
dc.type.degreeExamensarbete för kandidatexamensv
dc.type.degreeBachelor Thesisen
dc.type.uppsokM2
local.programmeSoftware Engineering (300 hp)
Ladda ner
Original bundle
Visar 1 - 1 av 1
Bild (thumbnail)
Namn:
251204.pdf
Storlek:
655.01 KB
Format:
Adobe Portable Document Format
Beskrivning:
Fulltext
Ladda ner
Samling
Examensarbeten för kandidatexamen