Rozhodovací procedury a verifikace – NAIL094

Výuka:	Letní semestr 2017/2018 Přednáška: Pondělí 9:00 S11 Cvičení: Pondělí 14:00 S6
Garantováno:	Katedra teoretické informatiky a matematické logiky
Zakončení:	Zkouška + Zápočet
Přednášející:	Martin Blicha (KDSS) e-mail: martin.blicha<at-sign>d3s.mff.cuni.cz
Informace v SIS:	NAIL094

Aktuality

• Cvičení zůstává v pondělí 14:00.
• Po prvním cvičení zůstaly nevyřešeny úkoly číslo 5 a 6. Tyto úkoly můžete odevzdávat do 4.3. 23:59 a získat za ně příslušný počet bodů.
• Byl zadán první úkol. Deadline: 11.3. 23:59
• Po druhém cvičení zůstaly nevyřešeny úkoly číslo 2 a 5. Tyto úkoly můžete odevzdávat do 11.3. 23:59 a získat za ně příslušný počet bodů.
• Byl zadán druhý úkol. Deadline: 8.4. 23:59
• Můžete odevzdávat úkoly číslo 3, 4 a 5 ze čtvrtého cvičení a úkol 3 ze třetího cvičení (kdo neviděl důkaz na cvičení). Deadline: 1.4. 23:59
• Můžete odevzdávat úkol číslo 3 z pátého cvičení. Deadline: 8.4. 23:59
• Byly zadány zbývající úkoly 3,4 a 5. Jde o rozšíření základního DPLL algoritmu, očekává se, že na konci bude mít solver, který obsahuje všechna rozšíření. Deadline: 20.5. 23:59
• Aktuální stav bodů zde. V případě nesrovnalostí nebo nejasností mě kontaktujte.

Přednášky

Datum	Název přednášky	Soubory
26.2.2018	Úvod, základní pojmy, normální formy, Tseitinovo kódování	Lecture01.pdf
5.3.2018	DPLL, CDCL	Lecture02.pdf
12.3.2018	dokončení DPLL frameworku, lokální SAT řešiče	Lecture03.pdf
19.3.2018	Binary decision diagrams, Quantified boolean formulas	Lecture04.pdf
26.3.2018	Satisfiability modulo theories (SMT)	Lecture05.pdf
9.4.2018	Logika s rovností a neinterpretovanými funkcemi	Lecture06.pdf
16.4.2018	Lineární aritmetika	Lecture07.pdf
23.4.2018	Aritmetika bitových polí (bit-vectors)	Lecture08.pdf
30.4.2018	Analýza programů	Lecture09.pdf
7.5.2018	Teorie polí a ukazatelů	Lecture10.pdf
14.5.2018	Kombinace teorií	Lecture11.pdf
21.5.2018	Interpolanty ve verifikaci	Lecture12.pdf

Cvičení

Datum	Název přednášky	Soubory
26.2.2018	Kódování problémů do SATu, Tseitinovo kódování	Seminar01.pdf
5.3.2018	Výroková splinitelnost	Seminar02.pdf
12.3.2018	Preprocessing a lokální prohledávání	Seminar03.pdf
19.3.2018	BDD, QBF	Seminar04.pdf
26.3.2018	Satisfiability modulo theories (SMT)	Seminar05.pdf
16.4.2018	Logika s rovností a neinterpretovanými funkcemi, algoritmus obecní simplex pro lineární aritmetiku	Seminar06.pdf
23.4.2018	Aritmetika bitových polí	Seminar07.pdf
30.4.2018	Analýza programů	Seminar08.pdf
7.5.2018	Teorie polí a ukazatelů	Seminar09.pdf
14.5.2018	Kombinace teorií	Seminar10.pdf
21.5.2018	Interpolanty ve verifikaci	Seminar11.pdf

Zápočet

Na zápočet je potřeba získat 35 bodů. Body se získávají především za programovací úkoly a také za úkoly zadávané na cvičeních.
Aktuální stav bodů zde.

Programovací úkoly

V průběhu semestru se budou postupně programovat základní algoritmy v moderních SAT solverech.

• Tseitinovo kódování (5b.)
• DPLL algoritmus (5b.)
• Watched literals (5b.)
• CDCL algoritmus (10b.)
• Heuristiky pro výběr proměnné (5b.)

Kromě těchto základních úkolů bude možné implementovat některé další algoritmy, které budou zveřejněny později.

Anotace

Přednáška o logických teoriích a procedurách rozhodujících splnitelnost v těchto teoriích s důrazem na aplikaci při verifikaci programů. Konstrukce efektivního SAT řešiče (DPLL, conflict-directed clause learning), lokální algoritmy splnitelnosti (WalkSAT, survey propagation), rozhodování v logice s rovností, s neinterpretovanými funkcemi a ukazateli, rozhodování ve výrokové logice s kvantifikátory (QBF), kombinování logických teorií, SAT-modulo řešiče.

Sylabus

• Úvod, motivace, základní pojmy. Normální formy formulí: CNF, DNF, NNF
• Problém splnitelnosti výrokové formule - SAT. Efektivní metody v moderních SAT řešičích. Lokální algoritmy splnitelnosti.
• Reprezentace booleovských funkcí pomocí BDD. Rozhodování ve výrokové logice s kvantifikátory: QBF
• Satisfiability modulo theory - SMT
• Rozhodovací procedury pro teorie prvořádové logiky: logika s rovností, teorie rovnosti a neinterpretovaných funkcí, teorie lineární aritmetiky, teorie polí a ukazatelů, teorie bitových polí.
• Kombinace logických teorií.

Literatura

• Daniel Kroening, Ofer Strichman: Decision Procedures: An Algorithmic Point of View. Springer, 2008.
• Aaron R. Bradley, Zohar Manna: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, 2007.
• Christel Baier, Joost-Pieter Katoen: Principles of Model Checking. The MIT Press, 2008.
• Edmund M. Clarke Jr., Orna Grumberg, Doron A. Peled: Model Checking. The MIT Press, 1999.
• Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh: Handbook of Satisfiability, IOS Press, 2009.