Model Checking Software - Ročkai, Petr (2015)
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