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

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

software

vyžadována - zdarma

Fiedor Tomáš, Ing., Ph.D. (UITS FIT VUT)
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Sinn Moritz, Dr. (FHS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Zuleger Florian, Dr. (FORSYTE)

Ranger je rozsireni nastroje Forester, ktery prevadi vstupni programy manipulujici s haldou do odpovidajicich aritmetickych program, ktere dale muzou byt analyzovany pomoci analyzeru konecnosti behu nebo mezi. Hlavni metoda je zalozena na hledani tzv. numerickych mer (normech), jako jsou napriklad delky listu nebo nejdelsi cesty ve strome, a na zaklade vysledku analyzy tvaru odvozuje mnozinu zmen v normech, ktere jsou dale transformovany na aritmeticke prikazy. Vysledne programy jsou pak analyzovany pomoci analyzatoru mezi (predevsim nastrojem Loopus). Precizni analyza zmen navic umoznuje zpracovat programy, ktere vyzaduji amortizovany pristup pro ziskani presnych mezi.

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

AQUAS: Agregované metody řízení kvality (8A17001)
Bezpečné a spolehlivé počítačové systémy (FIT-S-17-4014)
IT4Innovations excellence in science (LQ1602)
ROBUST - Verifikace a hledání chyb v pokročilém softwaru (GA17-12465S)

Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)

Fachhochschule St. Pölten (FHS)
FORSYTE, TU Wien (FORSYTE)
Ústav inteligentních systémů FIT VUT v Brně (UITS FIT VUT)