
QuickHeapsort
 Referenced in 11 articles
[sw20695]
 partitionphases and the analysis of the heapphases. 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: loopbound analysis, heapspace usage analysis and stack analysis ... utilises several thirdparty tools. Loop and heap bounds ... must be verified using KeY. Heapspace usage analysis requires COSTA. Stackspace 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 branchprediction 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 controlflow sensitivity (i.e., context, path, and heapsensitivity...

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 SecuriBenchmicro suite. The experimental...

THOR
 Referenced in 5 articles
[sw15079]
 that is capable of reasoning automatically about heapmanipulating 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 paramodulationbased 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 nontrivial 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 fixedpoint arithmetic...

ForwardDiff
 Referenced in 14 articles
[sw16106]
 vectorforward 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 provedsound Smallfootstyle program analysis for C minor, VeriStar demonstrates that fully ... mean that when the static analysis+theorem prover says a C minor program is safe ... stateoftheart 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 pointsto analysis regarding the derived types for variables...

Dafny
 Referenced in 72 articles
[sw00183]
 Dafny is an imperative objectbased 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...