SLAyer: Memory Safety for Systems-Level Code. SLAyer is a program analysis tool designed to automatically prove memory safety of industrial systems code. In this paper we describe SLAyer’s implementation, and its application to Windows device drivers. This paper accompanies the first release of SLAyer.
Keywords for this software
References in zbMATH (referenced in 11 articles )
Showing results 1 to 11 of 11.
- Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius: Automatically proving termination and memory safety for programs with pointer arithmetic (2017)
- Brotherston, James; Gorogiannis, Nikos; Kanovich, Max; Rowe, Reuben: Model checking for symbolic-heap separation logic with inductive predicates (2016)
- Dudka, Kamil; Holík, Lukáš; Peringer, Petr; Trtík, Marek; Vojnar, Tomáš: From low-level pointers to high-level containers (2016)
- Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
- Antonopoulos, Timos; Gorogiannis, Nikos; Haase, Christoph; Kanovich, Max; Ouaknine, Joël: Foundations for decision problems in separation logic with general inductive predicates (2014)
- Cox, Arlen; Chang, Bor-Yuh Evan; Sankaranarayanan, Sriram: Quicr: a reusable library for parametric abstraction of sets and numbers (2014)
- Berdine, Josh; Bjørner, Nikolaj; Ishtiaq, Samin; Kriener, Jael E.; Wintersteiger, Christoph M.: Resourceful reachability as HORN-LA (2013)
- Bjørner, Nikolaj: Taking satisfiability to the next level with Z3 (abstract) (2012)
- Stewart, Gordon; Beringer, Lennart; Appel, Andrew W.: Verified heap theorem prover by paramodulation (2012)
- Appel, Andrew W.: VeriSmall: verified Smallfoot shape analysis (2011) ioport
- Berdine, Josh; Cook, Byron; Ishtiaq, Samin: SLAyer: Memory safety for systems-level code (2011) ioport