Toward Verified Execution Environments. - William R. Bevier; Warren A. Hunt Jr.; William D. Young (S&P, 1987)

Kit and the Short Stack. - William R. Bevier (J. Autom. Reason., 1989)

An Approach to Systems Verification. - William R. Bevier; Warren A. Hunt Jr.; J Strother Moore; William D. Young (J. Autom. Reason., 1989)

Kit: A Study in Operating System Verification. - William R. Bevier (IEEE Trans. Software Eng., 1989)

Mechanically Checked Proofs of Kernel Specification. - William R. Bevier; Jørgen F. Søgaard-Andersen (CAV, 1991)

Machine Checked Proofs of the Design of a Fault-Tolerance Circuit. - William R. Bevier; William D. Young (Formal Aspects Comput., 1992)

A State-Based Approach to Non-Interference. - William D. Young; William R. Bevier (CSFW, 1994)

Connection policies and controlled interference. - William R. Bevier; Richard M. Cohen; William D. Young (CSFW, 1995)

A State-Machine Approach to Non-Interference. - William R. Bevier; William D. Young (J. Comput. Secur., 1995)

Mathematical Modeling and Analysis of an External Memory Manager. - William D. Young; William R. Bevier (FME, 1997)

The Specification-Based Testing of a Trusted Kernel: MK++. - Richard L. Ford; William R. Bevier; Richard T. Simon; Lawrence M. Smith (ICFEM, 1997)