Address spaces and virtual memory: specification, implementation, and correctness. - Mark Hillebrand (2007)