SLAyer: Memory Safety for Systems-level Code
- Josh Berdine ,
- Byron Cook ,
- Samin Ishtiaq
CAV |
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.