On the verification of memory management mechanisms

We define physical machines as processors with physical memory and swap memory; in user mode physical machines support address translation. We report about the formal verification of a complex processor supporting address translation by means of a memory management unit (MMU). We give a paper and pencil proof that physical machines togethe