papers
Publications (3)
cs.PL2025
Macaw: A Machine Code Toolbox for the Busy Binary Analyst
Ryan G. Scott, Brett Boston, Benjamin Davis +11
When attempting to understand the behavior of an executable, a binary analyst can make use of many different techniques. These include program slicing, dynamic instrumentation, bin…
cs.LO2014
Polymorphic Types in ACL2
Benjamin Selfridge, Eric Smith
This paper describes a tool suite for the ACL2 programming language which incorporates certain ideas from the Hindley-Milner paradigm of functional programming (as exemplified in p…
cs.LO2014
An ACL2 Mechanization of an Axiomatic Framework for Weak Memory
Benjamin Selfridge
Proving the correctness of programs written for multiple processors is a challenging problem, due in no small part to the weaker memory guarantees afforded by most modern architect…