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.)
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.