A preliminary evaluation of verifiability in Ada. - Anand R. Tripathi; William D. Young; Donald I. Good (ACM Annual Conference, 1980)

Generics and verification in Ada. - William D. Young; Donald I. Good (SIGPLAN, 1980)

HAL/S/V: a verifiable subset for HAL/S. - Anand R. Tripathi; William D. Young; Donald I. Good; James C. Browne (ACM SIGPLAN Notices, 1981)

Steelman and the verifiability of (preliminary) ADA. - William D. Young; Donald I. Good (ACM SIGPLAN Notices, 1981)

Secure Ada Target: Issues, System Design, and Verification. - William Earl Boebert; R. Y. Kaln; William D. Young; S. A. Hansohn (S&P, 1985)

Extending the Non-Interference Version of MLS for SAT. - J. Thomas Haigh; William D. Young (S&P, 1986)

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

Coding for a Believable Specification to Implementation Mapping. - William D. Young; John McHugh (S&P, 1987)

An Experience Using Two Covert Channel Analysis Techniques on a Real System Design. - J. Thomas Haigh; Richard A. Kemmerer; John McHugh; William D. Young (IEEE Trans. Software Eng., 1987)

Extending the Noninterference Version of MLS for SAT. - J. Thomas Haigh; William D. Young (IEEE Trans. Software Eng., 1987)

Verified Compilation in micro-Gypsy. - William D. Young (Symposium on Testing, Analysis, and Verification, 1989)

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

A Mechanically Verified Code Generator. - William D. Young (J. Autom. Reason., 1989)

Verified program support environments. - William D. Young (Formal Methods in Software Development, 1990)

Mathematical Methods for Digital Systems Development. - Donald I. Good; William D. Young (VDM Europe (2), 1991)

Formal Methods versus Software Engineering: Is There a Conflict? - William D. Young (Symposium on Testing, Analysis, and Verification, 1991)

Introduction to a Formally Defined Hardware Description Language. - Bishop Brock; Warren A. Hunt Jr.; William D. Young (TPCD, 1992)

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)

Comparing Verification Systems: Interactive Consistency in ACL2. - William D. Young (IEEE Trans. Software Eng., 1997)

Introducing Abstractions via Rewriting. - William D. Young (CHARME, 2005)

A robust machine code proof framework for highly secure applications. - David S. Hardin; Eric Whitman Smith; William D. Young (ACL2, 2006)

Mechanized Information Flow Analysis through Inductive Assertions. - Warren A. Hunt Jr.; Robert Bellarmine Krug; Sandip Ray; William D. Young (FMCAD, 2008)

Toward the Verification of a Simple Hypervisor - Mike Dahlin; Ryan Johnson 003; Robert Bellarmine Krug; Michael McCoyd; William D. Young (ACL2, 2011)

Building a Hypervisor on a Formally Verifiable Protection Layer. - Michael McCoyd; Robert Bellarmine Krug; Deepak Goel; Mike Dahlin; William D. Young (HICSS, 2013)

Modeling Asymptotic Complexity Using ACL2. - William D. Young (ACL2, 2022)