Sissejuhatus

Ajaline loogika: lineaarajaline loogika

Formaalne verifitseerimine algab süsteemi formaalse mudeli koostamisega. Formaliseeritakse soovitud omadused ning käitumine. Verifitseeritakse et mudel vastab spetsifikatsioonile.

Teoreemi tõestamine

Teoreemide tõestamise puhul on tegu formaalsete tõestuste mehhaniseerimisega. Interaktiivsed teoreemitõestajaid saab rakendada lõpmatutel süsteemidel (infinite systems). Teoreemi tõestaja (interaktiivne) võtab sisendiks mudeli M ning omadused P. Kui mõni omadus on rahuldamata siis teoreemi tõestada ei saa:

Kui kõik omadused on rahuldatud siis ongi teoreem tõestatud

Mudelikontroll

Vastunäide (counter example) on tee (trace) mis viib mõne omaduse (property) rikkumiseni.

Kui F on valem (formula) ning A on sobiv interperatsioon (fitting interpretation) valemile siis kui A tuletis A'(F) = True siis A on model valemile F.

Muutujatetele väärtuse omistamine V tähendab valmis muutujate asendamist. Interpretatsioon A on struktuur S koos omistatud muutujate väärtustega V.

propositional logic predicate logic

soundness of calculus completeness of calculus

Definition (satisfiable) A formula F is satisfiable if there exists a model for F .

Definition (valid) A formula F is valid, if each fitting interpretation of F is also a model of F . A valid formula is also called a tautology.

tuletamise reeglid (rules of inference)

lemma on abiteoreem

Rahultatavuse lahendamine (Satisfiability solving ehk SAT-solving) tuvastab kas Boole'i valem on rahuldatav. Muutujatele omistatakse väärtused, kasutatakse lihtsustusi (simplifications) ning tuletamisreegleid (rules of inference).

Satisfiability modulo theory ehk SMT on sisuliselt rahuldatavuse lahendamine taustateooria (background theory) abil. Taustateooria võib kätkeda võrdsust, interpreteerimata funktsioone, lineaararitmeetikat jne.