On the Verification of Memory Management Mechanisms

  • Iakov Dalinger
  • Mark Hillebrand
  • Wolfgang Paul
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)


We report on the design and 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 such a processor together with an appropriate page fault handler simulates virtual machines modeling user computation. These results are crucial steps towards the seamless verification of entire computer systems.


Virtual Machine Physical Machine Page Fault Address Translation Page Table 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Boyer, R.S., et al.: Special issue on system verification. (JAR) 5 (1989)Google Scholar
  2. 2.
    Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic Press, London (1988)zbMATHGoogle Scholar
  3. 3.
    Hunt, W.A.: Microprocessor design verification. In: JAR [1], pp. 429–460Google Scholar
  4. 4.
    Moore, J.S.: A mechanically verified language implementation. In: JAR [1], pp. 461–492Google Scholar
  5. 5.
    Young, W.D.: A mechanically verified code generator. In: JAR [1], pp. 493–518Google Scholar
  6. 6.
    Bevier, W.R.: Kit and the short stack. In: JAR [1], pp. 519–530Google Scholar
  7. 7.
    Moore, J.S.: A grand challenge proposal for formal methods: A verified stack. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 161–172. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  8. 8.
    The Verisoft Consortium: The Verisoft Project (2003),
  9. 9.
    Gargano, M., Hillebrand, M., Leinenbach, D., Paul, W.: On the correctness of operating system kernels. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 1–16. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  10. 10.
    Leinenbach, D., Paul, W., Petrova, E.: Towards the formal verification of a C0 compiler: Code generation and implementation correctness. In: Aichernig, B., Beckert, B. (eds.) SEFM  2005. IEEE Computer Society, Los Alamitos (2005)Google Scholar
  11. 11.
    Hillebrand, M., In der Rieden, T., Paul, W.: Dealing with I/O devices in the context of pervasive system verification. In: ICCD 2005. IEEE Computer Society, Los Alamitos (2005) (to appear)Google Scholar
  12. 12.
    Beyer, S., Jacobi, C., Kröning, D., Leinenbach, D., Paul, W.: Instantiating uninterpreted functional units and memory system: Functional verification of the VAMP. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 51–65. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  13. 13.
    Beyer, S.: Putting It All Together: Formal Verification of the VAMP. PhD thesis, Saarland University, Saarbrücken, Germany (2005)Google Scholar
  14. 14.
    Sawada, J., Hunt, W.A.: Processor verification with precise exceptions and speculative execution. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 135–146. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  15. 15.
    Müller, S.M., Paul, W.J.: Computer Architecture: Complexity and Correctness. Springer, Heidelberg (2000)zbMATHGoogle Scholar
  16. 16.
    Owre, S., Shankar, N., Rushby, J.M.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)Google Scholar
  17. 17.
    Aagaard, M., Ciubotariu, V., Higgins, J., Khalvati, F.: Combining equivalence verification and completion functions. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 98–112. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  18. 18.
    Paul, W., Dimova, D., Mancino, M.: Skript zur Vorlesung Systemarchitektur (2004),
  19. 19.
    Hillebrand, M.: Address Spaces and Virtual Memory: Specification, Implementation, and Correctnesss. PhD thesis, Saarland University, Saarbrücken, Germany (2005)Google Scholar
  20. 20.
    Kröning, D.: Formal Verification of Pipelined Microprocessors. PhD thesis, Saarland University, Saarbrücken, Germany (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Iakov Dalinger
    • 1
  • Mark Hillebrand
    • 1
  • Wolfgang Paul
    • 1
  1. 1.Computer Science Dept.Saarland UniversitySaarbrückenGermany

Personalised recommendations