Title :
Toward Verified Execution Environments
Author :
Bevier, William R. ; Hunt, Jr., Warren A. ; Young, William D.
Abstract :
Abstract: Current verification technology provides tools for the verification of programs written in a high-level language. Even verified high-level programs may not satisfy their specifications when executed, due to errors in tower-level software and hardware. We discuss an attempt at eliminating this problem with the design of an execution environment consisting of a compiler, operating system, and processor, each of which has been mechanically verified.
Keywords :
Abstracts; Assembly; Concrete; Finite element methods; Hardware; Operating systems; Virtual machining;
Conference_Titel :
Security and Privacy, 1987 IEEE Symposium on
Conference_Location :
Oakland, CA, USA
Print_ISBN :
0-8186-0771-8
DOI :
10.1109/SP.1987.10018
