Model Checking Software /
Systémy které navrhujeme jsou čím dál složitější a je často mimo lidské možnosti ověřit jejich korektnost. Výzkum v oblasti formálních metod vede k implementaci automatických nástrojů, které nám můžou s tímto úkolem pomoct. V současné době se však z různých důvodů užívá formálních metod pouze v ojed...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2015
|
| Témata: | |
| On-line přístup: | http://is.muni.cz/th/139761/fi_d/ |
| LEADER | 06480ctm a22011177i 4500 | ||
|---|---|---|---|
| 001 | MUB01006340907 | ||
| 003 | CZ BrMU | ||
| 005 | 20240515131515.0 | ||
| 008 | 150610s2015 xr ||||| |||||||||||eng d | ||
| STA | |a POSLANO DO SKCR |b 2016-03-09 | ||
| 035 | |a (ISMU-VSKP)188835 | ||
| 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 (0.034.2)004.4 |2 MRF | ||
| 080 | |a 004.03 |2 MRF | ||
| 080 | |a 004.438C++ |2 MRF | ||
| 080 | |a 004.052.42 |2 MRF | ||
| 080 | |a 004.421.032.24 |2 MRF | ||
| 080 | |a 004.43 |2 MRF | ||
| 100 | 1 | |a Ročkai, Petr |% UČO 139761 |* [absolvent FI MU] |4 dis | |
| 242 | 1 | 0 | |a Model Checking Software |y eng |
| 245 | 1 | 0 | |a Model Checking Software / |c Petr Ročkai |
| 264 | 0 | |c 2015 | |
| 300 | |a 188 stran | ||
| 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, 2015 | ||
| 520 | 2 | |a Systémy které navrhujeme jsou čím dál složitější a je často mimo lidské možnosti ověřit jejich korektnost. Výzkum v oblasti formálních metod vede k implementaci automatických nástrojů, které nám můžou s tímto úkolem pomoct. V současné době se však z různých důvodů užívá formálních metod pouze v ojedinělých případech. Obecným cílem této práce je zlepšit použitelnost metody ověřování modelu v návrhu a implementaci programů. Tato práce si klade za úkol přispět k dostupným znalostem v několika oblastech úzce spjatých s jejími cíly. V první řadě popisuje a implementuje interpret pro LLVM bitkód, který je centrální součástí nástroje pro ověřování programů. Poté uvede několik zlepšení tohoto základního interpretu: redkuce τ a τ+ pro zmenšení stavového prostoru vícevláknových programů, redukci pomocí symetrie haldy která činí dynamickou paměť praktickou a podporu výjimek nutnou pro verifikaci realistického kódu v jazyce C++. Za účelem zachycení složitého chování programů práce navrhuje nový j |% cze | |
| 520 | 2 | 9 | |a The systems we design are increasing in complexity and it is often beyond human capacity to verify their correctness. Research in formal methods has provided us with automated tools that can help ensure correctness of a system that is beyond our capabilities to check manually. Nowadays, for a variety of reasons, such tools are applied only to a very limited number of systems. The broad goal of this thesis is to improve applicability of model checking in design and implementation of general-purpose computer software. This thesis seeks to contribute to the state of the art in a number of areas closely aligned with this goal. Primarily, we describe and implement an interpreter for LLVM bitcode -- a centrepiece of a software model checker. We then introduce a number of improvements over the basic interpreter: τ and τ+ reduction to trim state spaces of threaded programs, heap symmetry reduction to make model checking with dynamic memory practical, exception handling which allows for verifi |9 eng |
| 650 | 0 | 7 | |a C++ (programovací jazyk) |7 ph116956 |2 czenas |
| 650 | 0 | 7 | |a počítačové systémy |7 ph115866 |2 czenas |
| 650 | 0 | 7 | |a software |7 ph125823 |2 czenas |
| 650 | 0 | 7 | |a formální verifikace |7 ph755479 |2 czenas |
| 650 | 0 | 7 | |a programovací jazyky |7 ph115890 |2 czenas |
| 650 | 0 | 7 | |a paralelní algoritmy |7 ph115668 |2 czenas |
| 650 | 0 | 9 | |a programming languages |2 eczenas |
| 650 | 0 | 9 | |a C++ (programming language) |2 eczenas |
| 650 | 0 | 9 | |a formal verification |2 eczenas |
| 650 | 0 | 9 | |a computer systems |2 eczenas |
| 650 | 0 | 9 | |a software |2 eczenas |
| 650 | 0 | 9 | |a parallel algorithms |2 eczenas |
| 655 | 7 | |a disertace |7 fd132024 |2 czenas | |
| 655 | 9 | |a dissertations |2 eczenas | |
| 658 | |a Informatika (čtyřleté) |b Počítačové systémy a technologie |c FI D-IN4 PST (PST) |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 http://is.muni.cz/th/139761/fi_d/ |
| CAT | |c 20150610 |l MUB01 |h 0421 | ||
| CAT | |a POSPEL |b 02 |c 20150625 |l MUB01 |h 0751 | ||
| CAT | |a HANAV |b 02 |c 20150811 |l MUB01 |h 1057 | ||
| CAT | |c 20150901 |l MUB01 |h 1453 | ||
| CAT | |a VESELA |b 02 |c 20150917 |l MUB01 |h 1012 | ||
| CAT | |c 20150921 |l MUB01 |h 1414 | ||
| CAT | |a VACOVAX |b 02 |c 20151012 |l MUB01 |h 1025 | ||
| CAT | |a POSPEL |b 02 |c 20151029 |l MUB01 |h 0733 | ||
| CAT | |a BATCH |b 00 |c 20151226 |l MUB01 |h 0545 | ||
| CAT | |c 20160303 |l MUB01 |h 1233 | ||
| CAT | |c 20160308 |l MUB01 |h 1504 | ||
| CAT | |c 20160309 |l MUB01 |h 1107 | ||
| CAT | |a POSPEL |b 02 |c 20160914 |l MUB01 |h 1427 | ||
| CAT | |a POSPEL |b 02 |c 20160920 |l MUB01 |h 0817 | ||
| CAT | |a POSPEL |b 02 |c 20160927 |l MUB01 |h 0741 | ||
| CAT | |a POSPEL |b 02 |c 20170228 |l MUB01 |h 1036 | ||
| CAT | |a POSPEL |b 02 |c 20170302 |l MUB01 |h 0828 | ||
| CAT | |a POSPEL |b 02 |c 20180314 |l MUB01 |h 0814 | ||
| CAT | |a POSPEL |b 02 |c 20180503 |l MUB01 |h 0729 | ||
| CAT | |a POSPEL |b 02 |c 20180710 |l MUB01 |h 0635 | ||
| CAT | |a POSPEL |b 02 |c 20190213 |l MUB01 |h 0800 | ||
| CAT | |a POSPEL |b 02 |c 20190924 |l MUB01 |h 0745 | ||
| CAT | |a SMUTNA |b 02 |c 20200317 |l MUB01 |h 0928 | ||
| CAT | |a POSPEL |b 02 |c 20200510 |l MUB01 |h 2306 | ||
| CAT | |a POSPEL |b 02 |c 20201212 |l MUB01 |h 2150 | ||
| CAT | |a POSPEL |b 02 |c 20210122 |l MUB01 |h 0054 | ||
| CAT | |a POSPEL |b 02 |c 20210322 |l MUB01 |h 1142 | ||
| CAT | |a POSPEL |b 02 |c 20210327 |l MUB01 |h 0026 | ||
| CAT | |c 20210614 |l MUB01 |h 1014 | ||
| CAT | |c 20210614 |l MUB01 |h 2002 | ||
| CAT | |a BATCH |b 00 |c 20210724 |l MUB01 |h 1238 | ||
| CAT | |a POSPEL |b 02 |c 20210912 |l MUB01 |h 2336 | ||
| CAT | |a POSPEL |b 02 |c 20211010 |l MUB01 |h 2218 | ||
| CAT | |a HANAV |b 02 |c 20211115 |l MUB01 |h 1631 | ||
| CAT | |a POSPEL |b 02 |c 20220629 |l MUB01 |h 0104 | ||
| CAT | |a POSPEL |b 02 |c 20221019 |l MUB01 |h 2326 | ||
| CAT | |a POSPEL |b 02 |c 20221101 |l MUB01 |h 0840 | ||
| CAT | |a POSPEL |b 02 |c 20230629 |l MUB01 |h 0037 | ||
| CAT | |a POSPEL |b 02 |c 20240226 |l MUB01 |h 1300 | ||
| CAT | |a POSPEL |b 02 |c 20240405 |l MUB01 |h 2123 | ||
| CAT | |a VESELAX |b 02 |c 20240515 |l MUB01 |h 1313 | ||
| CAT | |a VESELAX |b 02 |c 20240515 |l MUB01 |h 1314 | ||
| CAT | |a VESELAX |b 02 |c 20240515 |l MUB01 |h 1315 | ||
| LOW | |a POSLANO DO SKCR |b 2016-03-09 | ||
| 994 | - | 1 | |l MUB01 |l MUB01 |m VYSPR |1 FI |a Fakulta informatiky |2 SKLAD |b sklad |3 Diz. práce 2015 |5 42005D2660 |8 20150917 |f 72 |f Týdenní |r 20150917 |
| AVA | |a INF50 |b FI |c sklad |d Diz. práce 2015 |e available |t K dispozici |f 1 |g 0 |h N |i 1 |j SKLAD | ||