Thesis on verification of Fiasco's IPC implementation