IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL (Extended Version)

Matt Griffin, Brijesh Dongol, Azalea Raad

This paper presents IsaBIL, a binary analysis framework in Isabelle/HOL that is based on the widely used Binary Analysis Platform (BAP). Specifically, in IsaBIL, we formalise BAP's…