Formal Verification of Peripheral Memory Isolation

PhD thesis about formal verification (by means of interactive theorem proving) of memory isolation of I/O devices, that can be used to formally verify that device drivers configure their associated devices to access only certain memory regions.