DocumentCode
2562844
Title
Toward Verified Execution Environments
Author
Bevier, William R. ; Hunt, Jr., Warren A. ; Young, William D.
fYear
1987
fDate
27-29 April 1987
Firstpage
106
Lastpage
106
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Security and Privacy, 1987 IEEE Symposium on
Conference_Location
Oakland, CA, USA
ISSN
1540-7993
Print_ISBN
0-8186-0771-8
Type
conf
DOI
10.1109/SP.1987.10018
Filename
6234881
Link To Document