• QuickHeapsort

  • Referenced in 11 articles [sw20695]
  • partition-phases and the analysis of the heap-phases. This enables us to consider samples...
  • MLAT

  • Referenced in 3 articles [sw00582]
  • application of the framework for heap analysis...
  • ResAna

  • Referenced in 2 articles [sw13769]
  • types of resource analysis: loop-bound analysis, heap-space usage analysis and stack analysis ... utilises several third-party tools. Loop and heap bounds ... must be verified using KeY. Heap-space usage analysis requires COSTA. Stack-space analysis requires...
  • Valgrind

  • Referenced in 62 articles [sw04420]
  • instrumentation framework for building dynamic analysis tools. There are Valgrind tools that can automatically detect ... cache and branch-prediction profiler, and a heap profiler. It also includes three experimental tools...
  • Guppy 3

  • Referenced in 1 article [sw41043]
  • Guppy 3: A Python Programming Environment & Heap analysis toolset. Guppy 3 , a programming environment providing ... object and heap memory sizing, profiling and analysis. It includes a prototypical specification language that...
  • COSTA

  • Referenced in 24 articles [sw00162]
  • research prototype which performs automatic program analysis and which is able to infer cost ... amount of memory allocated on the heap, the number of bytecode instructions executed, the number ... executed by the program. When performing cost analysis, COSTA produces a cost equation system, which...
  • JSAI

  • Referenced in 6 articles [sw30521]
  • JSAI allows for analysis control-flow sensitivity (i.e., context-, path-, and heap-sensitivity...
  • CPAlien

  • Referenced in 2 articles [sw25255]
  • abstract domain for shape analysis of programs manipulating the heap. In particular, CPAlien extends SMGs...
  • Sails

  • Referenced in 1 article [sw34339]
  • combine the information leakage analysis with different heap abstractions, inferring information leakage over programs dealing ... data structures. We applied Sails to the analysis of the SecuriBench-micro suite. The experimental...
  • THOR

  • Referenced in 5 articles [sw15079]
  • that is capable of reasoning automatically about heap-manipulating programs. There are several such systems ... that it provides not only shape analysis, but also arithmetic reasoning via a novel combination...
  • VeriSmall

  • Referenced in 6 articles [sw09788]
  • VeriSmall: verified smallfoot shape analysis. We have implemented a version of the Smallfoot shape analyzer ... calling upon a paramodulation-based heap theorem prover. Our implementation is done...
  • Amortized Complexity

  • Referenced in 7 articles [sw28606]
  • Amortized Complexity Verified. A framework for the analysis of the amortized complexity of functional data ... folowing non-trivial ones: skew heaps, splay trees, splay heaps and pairing heaps. A preliminary...
  • QuickSpec

  • Referenced in 7 articles [sw19206]
  • based on testing, rather than static analysis or theorem proving. The main challenge QuickSpec faces ... generated using two case studies: a heap library for Haskell and a fixed-point arithmetic...
  • ForwardDiff

  • Referenced in 14 articles [sw16106]
  • vector-forward mode that avoids expensive heap allocation and makes better use of memory bandwidth ... fields such as astronomy, optimization, finite element analysis, and statistics. This document is an extended...
  • VeriStar

  • Referenced in 3 articles [sw09393]
  • Verified heap theorem prover by paramodulation. We present VeriStar, a verified theorem prover ... VeriSmall, a proved-sound Smallfoot-style program analysis for C minor, VeriStar demonstrates that fully ... mean that when the static analysis+theorem prover says a C minor program is safe ... state-of-the-art algorithm for deciding heap entailments and uses highly tuned verified functional...
  • TFA

  • Referenced in 1 article [sw38392]
  • proposing a new approach called type flow analysis (TFA) which propagates type information as well ... need to explicitly construct a heap abstraction. We have assessed our methodology from two perspectives ... standard Andersen’s subset based points-to analysis regarding the derived types for variables...
  • Dafny

  • Referenced in 72 articles [sw00183]
  • Dafny is an imperative object-based language with...
  • GAP

  • Referenced in 3154 articles [sw00320]
  • GAP is a system for computational discrete algebra...
  • gmp

  • Referenced in 282 articles [sw00363]
  • GMP is a free library for arbitrary precision...
  • LAPACK

  • Referenced in 1695 articles [sw00503]
  • LAPACK is written in Fortran 90 and provides...