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.