SLAyer: Memory Safety for Systems-level Code

Josh Berdine, Byron Cook, and Samin Ishtiaq

Abstract

SLAyer is a program analysis tool designed to automatically prove memory safety of industrial systems code. In this paper we describe SLAyer’s implementation as well as our experience applying the tool to Windows device drivers. This paper accompanies the first release of SLAyer.

Details

Publication typeInproceedings
Published inCAV
> Publications > SLAyer: Memory Safety for Systems-level Code