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 19 articles )

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

  1. Ta, Quang-Trung; Le, Ton Chanh; Khoo, Siau-Cheng; Chin, Wei-Ngan: Automated mutual induction proof in separation logic (2019)
  2. Duck, Gregory J.; Jaffar, Joxan; Yap, Roland H. C.: Shape neutral analysis of graph-based data-structures (2018)
  3. Jansen, Christina; Katelaan, Jens; Matheja, Christoph; Noll, Thomas; Zuleger, Florian: Unified reasoning about robustness properties of symbolic-heap separation logic (2017)
  4. Roşu, Grigore: Matching logic (2017)
  5. 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)
  6. Brotherston, James; Gorogiannis, Nikos; Kanovich, Max; Rowe, Reuben: Model checking for symbolic-heap separation logic with inductive predicates (2016)
  7. Dudka, Kamil; Holík, Lukáš; Peringer, Petr; Trtík, Marek; Vojnar, Tomáš: From low-level pointers to high-level containers (2016)
  8. Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: Deciding bit-vector formulas with mcsat (2016)
  9. Brotherston, James; Gorogiannis, Nikos: Disproving inductive entailments in separation logic via base pair approximation (2015)
  10. Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
  11. Antonopoulos, Timos; Gorogiannis, Nikos; Haase, Christoph; Kanovich, Max; Ouaknine, Joël: Foundations for decision problems in separation logic with general inductive predicates (2014)
  12. Cox, Arlen; Chang, Bor-Yuh Evan; Sankaranarayanan, Sriram: Quicr: a reusable library for parametric abstraction of sets and numbers (2014)
  13. Daniel, Jakub; Parízek, Pavel: Predicate abstraction in program verification: survey and current trends (2014)
  14. de Boer, Frank S.; de Gouw, Stijn: Combining monitoring with run-time assertion checking (2014)
  15. Berdine, Josh; Bjørner, Nikolaj; Ishtiaq, Samin; Kriener, Jael E.; Wintersteiger, Christoph M.: Resourceful reachability as HORN-LA (2013)
  16. Bjørner, Nikolaj: Taking satisfiability to the next level with Z3 (abstract) (2012)
  17. Stewart, Gordon; Beringer, Lennart; Appel, Andrew W.: Verified heap theorem prover by paramodulation (2012)
  18. Appel, Andrew W.: VeriSmall: verified Smallfoot shape analysis (2011) ioport
  19. Berdine, Josh; Cook, Byron; Ishtiaq, Samin: SLAyer: Memory safety for systems-level code (2011) ioport