An ACL2 Mechanization of an Axiomatic Framework for Weak Memory. - Benjamin Selfridge (ACL2, 2014)

Polymorphic Types in ACL2. - Benjamin Selfridge; Eric Smith (ACL2, 2014)

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)

BASALISC: Flexible Asynchronous Hardware Accelerator for Fully Homomorphic Encryption. - Robin Geelen; Michiel Van Beirendonck; Hilder V. L. Pereira; Brian Huffman; Tynan McAuley; Ben Selfridge; Daniel Wagner 001; Georgios D. Dimou; Ingrid Verbauwhede; Frederik Vercauteren; David W. Archer (IACR Cryptol. ePrint Arch., 2022)

BASALISC: Programmable Hardware Accelerator for BGV Fully Homomorphic Encryption. - Robin Geelen; Michiel Van Beirendonck; Hilder V. L. Pereira; Brian Huffman; Tynan McAuley; Ben Selfridge; Daniel Wagner 001; Georgios D. Dimou; Ingrid Verbauwhede; Frederik Vercauteren; David W. Archer (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2023)

Macaw: A Machine Code Toolbox for the Busy Binary Analyst. - Ryan G. Scott; Brett Boston; Benjamin Davis; Iavor S. Diatchki; Mike Dodds; Joe Hendrix; Daniel Matichuk; Kevin Quick; Tristan Ravitch; Valentin Robert; Benjamin Selfridge; Andrei Stefanescu; et al. (CoRR, 2024)