• SLAyer

  • Referenced in 21 articles [sw09712]
  • SLAyer: Memory Safety for Systems-Level Code. SLAyer is a program analysis tool designed ... automatically prove memory safety of industrial systems code. In this paper we describe SLAyer...
  • Infer

  • Referenced in 12 articles [sw20862]
  • Infer: An automatic program verifier for memory safety of C programs. Infer ... program verification tool aimed at proving memory safety of C programs. It attempts to build...
  • ESBMC

  • Referenced in 8 articles [sw09946]
  • about arithmetic under- and overflow, pointer safety, memory leaks, array bounds, atomicity and order violations...
  • Vellvm

  • Referenced in 6 articles [sw13286]
  • that hardens C programs against spatial memory safety violations. Vellvm’s tools allow...
  • AutoBayes/CC

  • Referenced in 4 articles [sw01806]
  • properties, e.g., operator safety or memory safety. Its basic idea is to require code producers...
  • HACL*

  • Referenced in 5 articles [sw36852]
  • each cryptographic primitive is verified for memory safety, mitigations against timing side-channels, and functional...
  • ARMor

  • Referenced in 4 articles [sw18275]
  • other, less-trusted components. ARMor guarantees memory safety and control flow integrity; it works...
  • GCminor

  • Referenced in 4 articles [sw22622]
  • support a simple but useful memory safety argument for this compiler, the front end uses...
  • VeriFast

  • Referenced in 66 articles [sw07705]
  • approach for the specification and verification of safety properties of pointer-manipulating imperative programs ... symbolic execution using an abstract representation of memory as a separation logic assertion. Folding...
  • CBMC

  • Referenced in 86 articles [sw09719]
  • allows verifying array bounds (buffer overflows), pointer safety, ex­cep­tions and user-specified ... embedded software, it also supports dynamic memory allocation using malloc and new. For questions about...
  • Cascade

  • Referenced in 3 articles [sw34344]
  • used to verify both memory safety as well as user-defined assertions. In this paper ... features such as its support for different memory models (trading off precision for scalability...
  • Crust

  • Referenced in 1 article [sw34343]
  • modern systems language that provides guaranteed memory safety through static analysis. However, Rust includes ... this code can lead to memory safety violations in parts of the program that ... bounded model checking to detect memory safety errors, as well as violations of Rust ... Rust standard library. It detects memory safety bugs that arose during the library’s development...
  • Sandcrust

  • Referenced in 1 article [sw35846]
  • decades. These languages are inherently unsafe regarding memory management. Even experienced developers make mistakes that ... open up security holes or compromise the safety properties of software. The Rust programming language ... systems domain and aims to eliminate memory-related programming errors by enforcing a strict memory ... library, which would otherwise invalidate the memory safety guarantees of Rust. Sandcrust is based...
  • Nagini

  • Referenced in 1 article [sw40594]
  • with new ideas, Nagini can verify memory safety, functional properties, termination, deadlock freedom, and input/output...
  • BakerSFIeld

  • Referenced in 1 article [sw23352]
  • concerns of rewriting the program for memory safety, and re-aligning the code for control...
  • Moat

  • Referenced in 1 article [sw23080]
  • incorrect use of SGX instructions or memory safety errors, can be exploited to divulge secrets...
  • SWATT

  • Referenced in 5 articles [sw09061]
  • compromise our privacy and safety by maliciously modifying the memory contents of these embedded devices...
  • NOrec

  • Referenced in 8 articles [sw24487]
  • present an ownership-record-free software transactional memory (STM) system that combines extremely low overhead ... that admits concurrent updates; publication and privatization safety; livelock freedom; a small, constant amount ... combines this set of features. While transactional memory for processors with hundreds of cores ... that require both closed nesting and publication safety...
  • Sycraft

  • Referenced in 7 articles [sw08199]
  • issue of distribution is addressed in shared-memory model where processes are constrained by their ... fault actions and a safety specification, the tool synthesizes a fault-tolerant program...
  • mist

  • Referenced in 2 articles [sw33293]
  • extensions. mist is tool to check safety properties against Petri Net like models. It implements ... graphs using d3js with runtime and memory consumption information...