A master thesis from Aalborg University
Pointer assertion logic & data structure invariant of MIR programs
Author(s)
Term
4. term
Education
Publication year
2023
Submitted on
2023-06-15
Pages
71 pages
Abstract
We investigate the use of the Pointer Assertion Logic Engine (PALE) in the context of Rust. We demonstrate how it is possible to translate Rust's Mid-Level Intermediate Representation (MIR) into the language PALE, where program annotations and Graph Types are used for semi-automatic formal reasoning over the program store, along with proof of Data Structure Invariants (DI) preservation. We provide a concrete example of modeling an intrusive circular doubly linked list data structure from the Rust-for-Linux project in PALE. We define DI over the said data structure, we attempted to show the absence of memory faults. In conclusion, we find that PALE, along with monadic second-order logic, is an interesting field for further exploration, although our transformation of MIR to PALE lacks a concrete proof of its validity.
Keywords
Documents
Colophon: This page is part of the AAU Student Projects portal, which is run by Aalborg University. Here, you can find and download publicly available bachelor's theses and master's projects from across the university dating from 2008 onwards. Student projects from before 2008 are available in printed form at Aalborg University Library.
If you have any questions about AAU Student Projects or the research registration, dissemination and analysis at Aalborg University, please feel free to contact the VBN team. You can also find more information in the AAU Student Projects FAQs.