• Operating system verification—An overview

    • Fulltext

       

        Click here to view fulltext PDF


      Permanent link:
      https://www.ias.ac.in/article/fulltext/sadh/034/01/0027-0069

    • Keywords

       

      Formal software verification; operating systems; theorem proving.

    • Abstract

       

      This paper gives a high-level introduction to the topic of formal, interactive, machine-checked software verification in general, and the verification of operating systems code in particular. We survey the state of the art, the advantages and limitations of machine-checked code proofs, and describe two specific ongoing larger-scale verification projects in more detail.

    • Author Affiliations

       

      Gerwin Klein1

      1. Sydney Research Laboratory, NICTA, Australia, School of Computer Science and Engineering, University of New South Wales, Sydney, Australia

© 2017 Indian Academy of Sciences, Bengaluru.