Υλοποίηση Μιας Μεθοδολογίας Αναλλοίωτων Βασισμένη Σε Backpointers

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.