Abstraction via Program Transformation /
V oblasti autonomní verifikace programů jsou abstrakční techniky nezbytné, protože hrají kritickou roli při snižování složitosti verifikačního procesu na zvládnutelné velikosti. Tyto techniky jsou však obvykle pevně integrovány do nástrojů, což vede k nežádoucí složitosti a opomenutí opakovaně použi...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2023
|
| Témata: | |
| On-line přístup: | https://is.muni.cz/th/mkjtn/ |
| Shrnutí: | V oblasti autonomní verifikace programů jsou abstrakční techniky nezbytné, protože hrají kritickou roli při snižování složitosti verifikačního procesu na zvládnutelné velikosti. Tyto techniky jsou však obvykle pevně integrovány do nástrojů, což vede k nežádoucí složitosti a opomenutí opakovaně použitelného návrhu. Pokud chce někdo použít konkrétní abstrakci v několika nástrojích, běžným přístupem je implementovat abstrakci zvlášť pro každý nástroj. To však vede k zbytečné duplikaci úsilí a nekonzistentním výsledkům, protože různé implementace se mohou lišit. Tato dizertační práce si klade za cíl řešit tuto výzvu vytvořením řešení pro snížení duplikace a složitosti abstrakce. Hlavním cílem je vytvořit nástrojově nezávislou abstrakci programu a využít ji k návrhu technik analýzy programu, které mohou být aplikovány libovolným nástrojem, čímž se snižuje složitost a umožňuje opakované použití abstrakce. To, co mají nástroje společné, je reprezentace programu, se kterou pracují. Jedna tako In the field of computer-aided verification, abstraction techniques are indispensable as they play a critical role in reducing the complexity of the verification process to manageable sizes. However, these techniques are usually tightly integrated into tools, resulting in undesired complexity and neglect of reusable design. If one wants to employ a particular abstraction in several tools, the common approach is to implement the abstraction separately for each tool. However, this results in unnecessary duplication of an effort and inconsistent results as different implementations may vary. This thesis aims to address this challenge by developing a solution to reduce the duplication and complexity of abstraction. The overarching objective is to create a tool-independent program abstraction and utilize it to design program analysis techniques that can be applied by any tool, thereby reducing its complexity and allowing abstraction reusability. What is common between tools is the program |
|---|---|
| Popis jednotky: | Vedoucí práce: Jiří Barnat |
| Fyzický popis: | 209 stran : ilustrace |