|
|
Template-Based Synthesis of Heap Abstractions
Malík, Viktor ; Hruška, Martin (referee) ; Vojnar, Tomáš (advisor)
Cieľom tejto práce je návrh analýzy tvaru haldy vhodnej pre potreby analyzátora 2LS. 2LS je nástroj pre analýzu C programov založený na automatickom odvodzovaní invariantov s použitím SMT solvera. Navrhované riešenie obsahuje spôsob reprezentácie tvaru programovej haldy pomocou logických formulí nad teóriou bitových vektorov. Tie sú následne využité v SMT solveri pre predikátovú logiku prvého rádu na odvodenie invariantov cyklov a súhrnov jednotlivých funkcií analyzovaného programu. Náš prístup je založený na ukazateľových prístupových cestách, ktoré vyjadrujú dosiahnuteľnosť objektov na halde z ukazateľových premenných. Informácie získané z analýzy môžu byť využité na dokázanie rôznych vlastností programu súvisiacich s prácou s dynamickýcmi dátovými štruktúrami. Riešenie bolo implementované v rámci nástroja 2LS. S jeho použitím došlo k výraznému zlepšeniu schopnosti 2LS analyzovať programy pracujúce s ukazateľmi a dynamickými dátovými štruktúrami. Toto je demonštrované na sade experimentov prevzatých zo známej medzinárodnej súťaže vo verifikácii programov SV-COMP a iných experimentoch.
|
|
|
Improving Precision of Program Analysis in the 2LS Framework
Smutný, Martin ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cílem této práce je navrhnout způsob vedoucí ke zvýšení přesnosti analýzy programů pomocí nástroje 2LS, založený na existujících konceptech, a to hlavně na syntézi invariant na základě šablon. 2LS je nástroj pro statickou analýzu programů napsaných v jazyce C, který využívá SMT solver a abstraktní interpretaci k automatickému odvození invariant. V případě kdy 2LS nedokáže rozhodnout zda je program správný, navrhované řešení analyzuje invarianty vypočítané v různých abstraktních doménách, a identifikuje takové části invariant, které mohou s největší pravděpodobností způsobit nejednoznačnost verifikace. Pomocí těchto získaných informací, dokáže navrhnutá metoda identifikovat proměnné původního programu, na kterých pravděpodobně závisí úspěch verifikace. Výstup tohoto řešení může posloužit jako zpětná vazba indikující proměnné, jejíchž problematické hodnoty by měly být omezeny. Také může být výstup využit vývojáři 2LS pro účely debugování při vývoji nových analýz. Řešení bylo implementováno v nástroji 2LS. Na základě různých experimentů mezinárodní soutěže ve verifikaci programů SV-COMP, dokáže řešení identifikovat proměnné způsobující nejednoznačnost verifikace ve více než polovině programů, na kterých verifikace momentálně selhává.
|
|
|
Improving Precision of Program Analysis in the 2LS Framework
Smutný, Martin ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cílem této práce je navrhnout způsob vedoucí ke zvýšení přesnosti analýzy programů pomocí nástroje 2LS, založený na existujících konceptech, a to hlavně na syntézi invariant na základě šablon. 2LS je nástroj pro statickou analýzu programů napsaných v jazyce C, který využívá SMT solver a abstraktní interpretaci k automatickému odvození invariant. V případě kdy 2LS nedokáže rozhodnout zda je program správný, navrhované řešení analyzuje invarianty vypočítané v různých abstraktních doménách, a identifikuje takové části invariant, které mohou s největší pravděpodobností způsobit nejednoznačnost verifikace. Pomocí těchto získaných informací, dokáže navrhnutá metoda identifikovat proměnné původního programu, na kterých pravděpodobně závisí úspěch verifikace. Výstup tohoto řešení může posloužit jako zpětná vazba indikující proměnné, jejíchž problematické hodnoty by měly být omezeny. Také může být výstup využit vývojáři 2LS pro účely debugování při vývoji nových analýz. Řešení bylo implementováno v nástroji 2LS. Na základě různých experimentů mezinárodní soutěže ve verifikaci programů SV-COMP, dokáže řešení identifikovat proměnné způsobující nejednoznačnost verifikace ve více než polovině programů, na kterých verifikace momentálně selhává.
|
|
|
Template-Based Synthesis of Heap Abstractions
Malík, Viktor ; Hruška, Martin (referee) ; Vojnar, Tomáš (advisor)
Cieľom tejto práce je návrh analýzy tvaru haldy vhodnej pre potreby analyzátora 2LS. 2LS je nástroj pre analýzu C programov založený na automatickom odvodzovaní invariantov s použitím SMT solvera. Navrhované riešenie obsahuje spôsob reprezentácie tvaru programovej haldy pomocou logických formulí nad teóriou bitových vektorov. Tie sú následne využité v SMT solveri pre predikátovú logiku prvého rádu na odvodenie invariantov cyklov a súhrnov jednotlivých funkcií analyzovaného programu. Náš prístup je založený na ukazateľových prístupových cestách, ktoré vyjadrujú dosiahnuteľnosť objektov na halde z ukazateľových premenných. Informácie získané z analýzy môžu byť využité na dokázanie rôznych vlastností programu súvisiacich s prácou s dynamickýcmi dátovými štruktúrami. Riešenie bolo implementované v rámci nástroja 2LS. S jeho použitím došlo k výraznému zlepšeniu schopnosti 2LS analyzovať programy pracujúce s ukazateľmi a dynamickými dátovými štruktúrami. Toto je demonštrované na sade experimentov prevzatých zo známej medzinárodnej súťaže vo verifikácii programov SV-COMP a iných experimentoch.
|
guest ::
