Product Details
Ranger: A Tool for Bounds Analysis of Heap-Manipulating Programs
Created: 2018
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT)
Sinn Moritz, Dr. (FHS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Zuleger Florian, Dr. (FORSYTE)
forest automata
bounds analysis
arithmetic program generation
shape analysis
amortized complexity
numerical measures
Ranger is an extension of the Forester tool, which transforms input heap-manipulating programs into corresponding arithmetic programs, which can be subsequently analysed using termination or bounds analysers. Its method is based on finding so called numerical measures (norms), such as lengths of lists or longest paths in trees, and based on results of shape analysis infer a set of changes, which are subsequently transformed to arithmetic statements. The resulting programs are then analysed using bounds analyser (in particular, the Loopus tool). The precise handling of the changes allows analysis of programs requiring amortized reasoning.
The tool and manual is located at http://www.fit.vutbr.cz/research/groups/verifit/tools/ranger/ and at https://pajda.fit.vutbr.cz/ifiedortom/forester-resource-bounds
Free software under the terms of GNU GPL (cf.http://www.gnu.org/licenses/gpl.html).
IT4Innovations excellence in science (LQ1602)
ROBUST - veRificatiOn and Bug hUnting for advanced SofTware (GA17-12465S)
Secure and Reliable Computer Systems (FIT-S-17-4014)
FORSYTE, TU Wien (FORSYTE)
St. Pölten University of Applied Sciences (FHS)