Počet záznamů: 1
Aplikace bez chyby
Údaje o názvu Aplikace bez chyby [rukopis] / Ondřej Vaverka Další variantní názvy Aplikace bez chyby Osobní jméno Vaverka, Ondřej (autor diplomové práce nebo disertace) Překl.náz A flawless application Vyd.údaje 2012 Fyz.popis 57 s. + 1 CD s textem bakalářské práce a s programy Pheasant a File synchronizer Poznámka Ved. práce Michal Krupka Oponent Petr Osička Dal.odpovědnost Krupka, Michal (vedoucí diplomové práce nebo disertace) Osička, Petr (oponent) Dal.odpovědnost Univerzita Palackého. Katedra informatiky (udelovatel akademické hodnosti) Klíč.slova formální kontrola správnosti programů * weakest preconditions * automatická verifikace programů * důkaz správnosti programu * formal software verification * weakest preconditions * automatic software verification * proof of program correctness Forma, žánr bakalářské práce bachelor's theses MDT (043)378.22 Země vyd. Česko Jazyk dok. čeština Druh dok. PUBLIKAČNÍ ČINNOST Titul Bc. Studijní program Bakalářský Studijní program Informatika Studijní obor Informatika kniha
Kvalifikační práce Staženo Velikost datum zpřístupnění 00171504-838235626.pdf 49 293.3 KB 23.05.2012 Posudek Typ posudku 00171504-opon-228913326.pdf Posudek oponenta
Tato práce se zabývá možnostmi formální kontroly správnosti programů. Nejprve jsou stručně popsány základní přístupy k ověřování správnosti programů, jakými jsou například model checking nebo theorem proving. V další části se práce věnuje problémům spojeným s ověřováním programů pomocí weakest precondition a uvádí existujicí způsoby řešení. V této části je také představen experimentální verifikátor programů Pheasant, který vznikl jako součást této bakalářské práce. Poslední kapitola se věnuje jednoduchému synchronizačnímu nástroji, především pak formálnímu důkazu správnosti algoritmu, na kterém je tento nástroj postaven. Implementace tohoto algoritmu je poté úspěšně automaticky ověřena verifikátorem Pheasant.The topic of this bachelor thesis is formal software verification. It contains a concise description of basic verification methods like model checking or theorem proving. The next chapter focuses on issues associated with software verification using weakest preconditions and presents existing solutions for these issues. The Pheasant - experimental software verificator that was created as a part of this thesis - is introduced in this chapter. The last part describes very simple file synchronizer, especially the proof of correctness of its main algorithm. The correctness of algorithm implementation is automatically proved with Pheasant.
Počet záznamů: 1