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

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

software

K využití výsledku jiným subjektem je vždy nutné nabytí licence

Poskytovatel licence na výsledek nepožaduje licenční poplatek

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

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

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, EU, Horizon 2020, 8A17001, 737475, 2017-2020, ukončen
Bezpečné a spolehlivé počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-17-4014, 2017-2020, ukončen
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, 2016-2020, ukončen
ROBUST - Verifikace a hledání chyb v pokročilém softwaru, GAČR, Standardní projekty, GA17-12465S, 2017-2019, řešení

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

Ústav inteligentních systémů (UITS)