Ranger: A Tool for Bounds Analysis of Heap-Manipulating Programs

Czech title

Ranger: Nástroj pro Analýzu Mezí Programů Manipulujících s Haldou

Type

software

License

In order to use the result by another entity, it is always necessary to acquire a license

License Fee

The licensor does not require a license fee for the result

Authors

Fiedor Tomáš, Ing., Ph.D. (RG VERIFIT)
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Sinn Moritz (FIT)
Zuleger Florian, Dr. (FIT)

Keywords

forest automata bounds analysis arithmetic program generation shape analysis amortized complexity numerical measures

Description

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.

Location

Nástroj a dodatečné informace se nacházejí na http://www.fit.vutbr.cz/research/groups/verifit/tools/ranger/ a https://pajda.fit.vutbr.cz/ifiedortom/forester-resource-bounds

License Conditions

Free software under the terms of GNU GPL (cf.http://www.gnu.org/licenses/gpl.html).

Projects

AQUAS: Aggregated Quality Assurance for Systems, EU, Horizon 2020, 8A17001, 737475, 2017-2020, completed
Bezpečné a spolehlivé počítačové systémy, BUT, Vnitřní projekty VUT, FIT-S-17-4014, 2017-2020, completed
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, 2016-2020, completed
ROBUST - veRificatiOn and Bug hUnting for advanced SofTware, GACR, Standardní projekty, GA17-12465S, 2017-2019, running

Research groups

Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)

Departments

Department of Intelligent Systems (DITS)