Number of the records: 1
Aplikace bez chyby
Title statement Aplikace bez chyby [rukopis] / Ondřej Vaverka Additional Variant Titles Aplikace bez chyby Personal name Vaverka, Ondřej (dissertant) Translated title A flawless application Issue data 2012 Phys.des. 57 s. + 1 CD s textem bakalářské práce a s programy Pheasant a File synchronizer Note Ved. práce Michal Krupka Oponent Petr Osička Another responsib. Krupka, Michal (thesis advisor) Osička, Petr (opponent) Another responsib. Univerzita Palackého. Katedra informatiky (degree grantor) Keywords 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 Form, Genre bakalářské práce bachelor's theses UDC (043)378.22 Country Česko Language čeština Document kind PUBLIKAČNÍ ČINNOST Title Bc. Degree program Bakalářský Degree program Informatika Degreee discipline Informatika book
Kvalifikační práce Downloaded Size 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.
Number of the records: 1