Abstrakce dynamických datových struktur s využitím šablon
| Autor: | Malík, Viktor |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: |
analýza založená na šablónach
shape analysis prístupové cesty na halde program analysis abstraktná interpretácia zreťazené zoznamy formal verification invariant inference linked lists súhrny funkcií abstract interpretation formálna verifikácia dynamic data structures SSA forma odvodzovanie invariantov analýza programov template-based analysis 2LS dynamické dátové štruktúry pointer access paths analýza tvaru haldy SSA form function summaries |
| Druh dokumentu: | masterThesis |
| Popis: | 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. |
| Databáze: | Networked Digital Library of Theses & Dissertations |
| Externí odkaz: |
|