SLAyer

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.


References in zbMATH (referenced in 15 articles )

Showing results 1 to 15 of 15.
Sorted by year (citations)

  1. Jansen, Christina; Katelaan, Jens; Matheja, Christoph; Noll, Thomas; Zuleger, Florian: Unified reasoning about robustness properties of symbolic-heap separation logic (2017)
  2. 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)
  3. Brotherston, James; Gorogiannis, Nikos; Kanovich, Max; Rowe, Reuben: Model checking for symbolic-heap separation logic with inductive predicates (2016)
  4. Dudka, Kamil; Holík, Lukáš; Peringer, Petr; Trtík, Marek; Vojnar, Tomáš: From low-level pointers to high-level containers (2016)
  5. Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: Deciding bit-vector formulas with mcsat (2016)
  6. Brotherston, James; Gorogiannis, Nikos: Disproving inductive entailments in separation logic via base pair approximation (2015)
  7. Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
  8. Antonopoulos, Timos; Gorogiannis, Nikos; Haase, Christoph; Kanovich, Max; Ouaknine, Joël: Foundations for decision problems in separation logic with general inductive predicates (2014)
  9. Cox, Arlen; Chang, Bor-Yuh Evan; Sankaranarayanan, Sriram: Quicr: a reusable library for parametric abstraction of sets and numbers (2014)
  10. de Boer, Frank S.; de Gouw, Stijn: Combining monitoring with run-time assertion checking (2014)
  11. Berdine, Josh; Bjørner, Nikolaj; Ishtiaq, Samin; Kriener, Jael E.; Wintersteiger, Christoph M.: Resourceful reachability as HORN-LA (2013)
  12. Bjørner, Nikolaj: Taking satisfiability to the next level with Z3 (abstract) (2012)
  13. Stewart, Gordon; Beringer, Lennart; Appel, Andrew W.: Verified heap theorem prover by paramodulation (2012)
  14. Appel, Andrew W.: VeriSmall: verified Smallfoot shape analysis (2011) ioport
  15. Berdine, Josh; Cook, Byron; Ishtiaq, Samin: SLAyer: Memory safety for systems-level code (2011) ioport