SMT Solving for the Theory of Bit-Vectors
Martin Jonáš · 2016
Teze me dizertacni prace se zabývaji rozhodovanim splnitelnosti formuli logiky prvniho řadu nad teorii bitových vektorů. Teze nejprve popisuji soucasně použivane přistupy k řeseni splnitelnosti formuli výrokove logiky a prvořadových formuli nad danou teorii. Pote se věnuji postupům použivaným konkretně při řeseni splnitelnosti formuli nad teorii bitových vektorů, a to jak formuli bez kvantifikatorů, tak i formuli s kvantifikatory. Zminěny jsou take zname výsledky o výpocetni složitosti několika variant problemu splnitelnosti formuli nad teori bitových vektorů. V tezich je dale popsan nas publikovaný výzkum v oblasti symbolických algoritmů pro řeseni splnitelnosti kvantifikovaných formuli nad teorii bitových vektorů a navrženy možnosti jeho rozsiřeni. Nejpodstatnějsi možnosti rozsiřeni je hybridni přistup, který kombinuje symbolickou reprezentaci casti formule se znamými algoritmy založenými na hledani přiřazeni, ktere splňuje zadanou formuli.