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.

PDF file

In  CAV

Details