This repository contains all sources for my thesis: Verification of Fiasco's IPC implementation. This includes the LaTeX sources for the thesis, the source code that was modelled and the PVS model and its proofs.