Linear and Nonlinear Arithmetic in ACL2. - Warren A. Hunt Jr.; Robert Bellarmine Krug; J Strother Moore (CHARME, 2003)

Meta Reasoning in ACL2. - Warren A. Hunt Jr.; Matt Kaufmann; Robert Bellarmine Krug; J Strother Moore; Eric Whitman Smith (TPHOLs, 2005)

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)