Adding parallelism capabilities to ACL2. - David L. Rager (ACL2, 2006)

A Futures Library and Parallelism Abstractions for a Functional Subset of Lisp. - David L. Rager; Warren A. Hunt Jr.; Matt Kaufmann (ELS, 2011)

A Parallelized Theorem Prover for a Logic with Parallel Execution. - David L. Rager; Warren A. Hunt Jr.; Matt Kaufmann (ITP, 2013)

Formal verification of division and square root implementations, an Oracle report. - David L. Rager; Jo C. Ebergen; Dmitry Nadezhin; Austin Lee; Cuong Kim Chau; Ben Selfridge (FMCAD, 2016)