Please use this identifier to cite or link to this item:
http://artemis.cslab.ece.ntua.gr:8080/jspui/handle/123456789/16501
Title: | Υλοποίηση Μιας Μεθοδολογίας Αναλλοίωτων Βασισμένη Σε Backpointers |
Authors: | Ελευθέριος Κρητικός Παπασπύρου Νικόλαος |
Keywords: | backpointers chalice verification specification copy-on-write lists formal methods framing problem implicit dynamic frames fictional disjoint datastructures priority inheritance prolocol |
Issue Date: | 28-Nov-2012 |
Abstract: | Solid guarantees that a computer program will behave the desired way is onlypossible by formal verification. As the complexity of designs growsexponentially and computer systems are used in critical applications, it becomesincreasingly important to prove the correctness of algorithms.One of the most challenging problems in formal specification and verificationis the framing problem. In this thesis we propose an new formalism thatextends the current methodologies targeting the framing problem: Backpointers.Backpointers increase the expressiveness by allowing specifications to includeobjects not accessible from the current stack. We implemented this approach inChalice, an object-oriented and concurrent specification language that usesimplicit dynamic frames and fractional permissions. Finally, by using thisextension of Chalice we worked on proving the validity of a concurrentimplementation of copy-on-write lists and the priority inheritance protocol. Tothe best of our knowledge this is the first attempt to prove a program fromthis family of problems using an automated verifier. |
URI: | http://artemis-new.cslab.ece.ntua.gr:8080/jspui/handle/123456789/16501 |
Appears in Collections: | Διπλωματικές Εργασίες - Theses |
Files in This Item:
File | Size | Format | |
---|---|---|---|
DT2012-0293.pdf | 729.5 kB | Adobe PDF | View/Open |
Items in Artemis are protected by copyright, with all rights reserved, unless otherwise indicated.