• Top
    • Documentation
      • Xdoc
      • ACL2-doc
      • Recursion-and-induction
      • Loop$-primer
      • Operational-semantics
        • Operational-semantics-3__annotated-bibliography
          • Bib::bhmy89
          • Bib::liu06
          • Bib::bm96
          • Bib::plotkin04b
          • Bib::bgm90
          • Bib::hkms17
          • Bib::bkm96
          • Bib::moore15
          • Bib::bh99
          • Bib::wilding93
          • Bib::plotkin04a
          • Bib::moore03b
          • Bib::mp02
          • Bib::moore19
          • Bib::manolios00
          • Bib::flatau92
          • Bib::hb92
          • Bib::bm05
          • Bib::goel16
          • Bib::bm73
          • Bib::ghk17
          • Bib::wilding92
          • Bib::moore17
          • Bib::moore96
          • Bib::ghkg14
          • Bib::yu92
          • Bib::hunt85
          • Bib::boh03
          • Bib::mmrv06
          • Bib::bm80
          • Bib::bh97
          • Bib::moore99b
          • Bib::moore14
          • Bib::rm04
          • Bib::by96
          • Bib::sawada00
          • Bib::mccarthy62
          • Bib::bm79
          • Bib::moore99a
          • Bib::sh98
          • Bib::rhmm07
          • Bib::kmm00a
          • Bib::ghk13
          • Bib::moore03a
          • Bib::hk12
          • Bib::mp67
          • Bib::young88
          • Bib::bm97
          • Bib::moore73
          • Bib::kmm00b
          • Bib::bevier87
          • Operational-semantics-1__simple-example
          • Operational-semantics-2__other-examples
          • Operational-semantics-5__history-etc
          • Operational-semantics-4__how-to-find-things
        • Pointers
        • Doc
        • Documentation-copyright
        • Course-materials
        • Args
        • ACL2-doc-summary
        • Finding-documentation
        • Broken-link
        • Doc-terminal-test-2
        • Doc-terminal-test-1
      • Books
      • Boolean-reasoning
      • Projects
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Operational-semantics-3__annotated-bibliography

    Bib::bevier87

    W. R. Bevier, Verified Operating System Kernel (ftp://ftp.cs.utexas.edu/pub/boyer/diss/bevier.pdf), University of Texas at Austin, Ph.D. dissertation, 1987.



    Relevance: first verified operating system and a component of the CLI stack



    ———

    The verified operating system kernel used in the CLI Verified Stack as reported in bib::bhmy89 is described here.

    See the Nqthm script examples/bevier/kit.events.