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.
| Identifer | oai:union.ndltd.org:nusl.cz/oai:invenio.nusl.cz:363894 |
| Date | January 2017 |
| Creators | Malík, Viktor |
| Contributors | Hruška, Martin, Vojnar, Tomáš |
| Publisher | Vysoké učení technické v Brně. Fakulta informačních technologií |
| Source Sets | Czech ETDs |
| Language | English |
| Detected Language | Unknown |
| Type | info:eu-repo/semantics/masterThesis |
| Rights | info:eu-repo/semantics/restrictedAccess |
Page generated in 0.0026 seconds