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/ |
| LEADER | 04789ctm a22006857i 4500 | ||
|---|---|---|---|
| 001 | MUB01006534998 | ||
| 003 | CZ BrMU | ||
| 005 | 20241120110756.0 | ||
| 008 | 240221s2023 xr ||||| |||||||||||eng d | ||
| STA | |a POSLANO DO SKCR |b 2024-07-15 | ||
| 035 | |a (ISMU-VSKP)310575 | ||
| 040 | |a BOD114 |b cze |d BOD018 |e rda | ||
| 072 | 7 | |a 004.4/.6 |x Programování. Software |2 Konspekt |9 23 | |
| 080 | |a 004 |2 MRF | ||
| 080 | |a 004.42 |2 MRF | ||
| 080 | |a 004.4 |2 MRF | ||
| 080 | |a 004.94 |2 MRF | ||
| 080 | |a 004.43 |2 MRF | ||
| 080 | |a 004.438C++ |2 MRF | ||
| 100 | 1 | |a Lauko, Henrich |% UČO 410438 |* [absolvent FI MU] |4 dis | |
| 242 | 1 | 0 | |a Abstraction via Program Transformation |y eng |
| 245 | 1 | 0 | |a Abstraction via Program Transformation / |c Henrich Lauko |
| 264 | 0 | |c 2023 | |
| 300 | |a 209 stran : |b ilustrace | ||
| 336 | |a text |b txt |2 rdacontent | ||
| 337 | |a bez média |b n |2 rdamedia | ||
| 338 | |a svazek |b nc |2 rdacarrier | ||
| 500 | |a Vedoucí práce: Jiří Barnat | ||
| 502 | |a Dizertace (Ph.D.)--Masarykova univerzita, Fakulta informatiky, 2024 | ||
| 520 | 2 | |a 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 |% cze | |
| 520 | 2 | 9 | |a 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 |9 eng |
| 650 | 0 | 7 | |a výpočetní technika |7 ph137273 |2 czenas |
| 650 | 0 | 7 | |a programování |7 ph115891 |2 czenas |
| 650 | 0 | 7 | |a modelování a simulace |7 ph125543 |2 czenas |
| 650 | 0 | 7 | |a programovací jazyky |7 ph115890 |2 czenas |
| 650 | 0 | 7 | |a C++ (programovací jazyk) |7 ph116956 |2 czenas |
| 650 | 0 | 9 | |a computer science |2 eczenas |
| 650 | 0 | 9 | |a programming |2 eczenas |
| 650 | 0 | 9 | |a modelling and simulation |2 eczenas |
| 650 | 0 | 9 | |a programming languages |2 eczenas |
| 650 | 0 | 9 | |a C++ (programming language) |2 eczenas |
| 655 | 7 | |a disertace |7 fd132024 |2 czenas | |
| 655 | 9 | |a dissertations |2 eczenas | |
| 658 | |a Informatika |b Technologie a metodologie počítačových systémů |c FI D-INF DIIA (DIIA) |2 CZ-BrMU | ||
| 700 | 1 | |a Barnat, Jiří, |d 1977- |7 mub2010575337 |% UČO 3496 |4 ths | |
| 710 | 2 | |a Masarykova univerzita. |b Katedra teorie programování |4 dgg | |
| 856 | 4 | 1 | |u https://is.muni.cz/th/mkjtn/ |
| CAT | |c 20240221 |l MUB01 |h 0420 | ||
| CAT | |a POSPEL |b 02 |c 20240223 |l MUB01 |h 0927 | ||
| CAT | |a POSPEL |b 02 |c 20240226 |l MUB01 |h 1300 | ||
| CAT | |a POSPEL |b 02 |c 20240405 |l MUB01 |h 2124 | ||
| CAT | |a VESELA |b 02 |c 20240410 |l MUB01 |h 0942 | ||
| CAT | |c 20240715 |l MUB01 |h 1016 | ||
| CAT | |a VESELA |b 02 |c 20241120 |l MUB01 |h 1107 | ||
| CAT | |a VESELA |b 02 |c 20241120 |l MUB01 |h 1107 | ||
| CAT | |a REPISOVA |b 02 |c 20251024 |l MUB01 |h 1418 | ||
| LOW | |a POSLANO DO SKCR |b 2024-07-15 | ||
| 994 | - | 1 | |l MUB01 |l MUB01 |m VYSPR |1 FI |a Fakulta informatiky |2 SKLAD |b sklad |3 Doktorská práce 2023 |5 42005D2774 |8 20240410 |f 72 |f Týdenní |r 20240410 |
| AVA | |a INF50 |b FI |c sklad |d Doktorská práce 2023 |e available |t K dispozici |f 1 |g 0 |h N |i 0 |j SKLAD | ||