| 2025 | FMCAD | A Formal Y86 Simulator with CHERI Features. | Carl Kwan, Yutong Xin, William D. Young |
| 2008 | FMCAD | Mechanized Information Flow Analysis through Inductive Assertions. | Warren A. Hunt Jr., Robert Bellarmine Krug, Sandip Ray, William D. Young |
| 1997 | FM | Mathematical Modeling and Analysis of an External Memory Manager. | William D. Young, William R. Bevier |
| 1991 | FM | Mathematical Methods for Digital Systems Development. | Donald I. Good, William D. Young |
| 1991 | ISSTA | Formal Methods versus Software Engineering: Is There a Conflict? | William D. Young |
| 1989 | ISSTA | Verified Compilation in micro-Gypsy. | William D. Young |
| 1987 | SP | Toward Verified Execution Environments. | William R. Bevier, Warren A. Hunt Jr., William D. Young |
| 1987 | SP | Coding for a Believable Specification to Implementation Mapping. | William D. Young, John McHugh |
| 1986 | SP | An Experience Using Two Covert Channel Analysis Techniques on a Real System Design. | J. Thomas Haigh, Richard A. Kemmerer, John McHugh, William D. Young |
| 1986 | SP | Extending the Non-Interference Version of MLS for SAT. | J. Thomas Haigh, William D. Young |
| 1985 | SP | Secure Ada Target: Issues, System Design, and Verification. | William Earl Boebert, R. Y. Kaln, William D. Young, S. A. Hansohn |