Rozhodovací procedury a verifikace - NAIX094

• Anglický název: Decision Procedures and Verification
• Zajišťuje: Studijní oddělení (32-STUD)
• Fakulta: Matematicko-fyzikální fakulta
• Platnost: od 2022
• Semestr: letní
• E-Kredity: 6
• Rozsah, examinace: letní s.:2/2, Z+Zk [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• 4EU+: ne
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• Stav předmětu: vyučován
• Jazyk výuky: čeština
• Způsob výuky: prezenční
• Je zajišťováno předmětem: NAIL094
• Další informace: http://ktiml.mff.cuni.cz/~kucerap/satsmt/
• Garant: RNDr. Petr Kučera, Ph.D.
• Třída: Informatika Mgr. - volitelný
• Kategorizace předmětu: Informatika > Teoretická informatika
• Prerekvizity : {NXXX036, NXXX037, NXXX038, NXXX039, NXXX040, NXXX067, NXXX069}
• Neslučitelnost : NAIL094
• Záměnnost : NAIL094
• Je neslučitelnost pro: NAIL094
• Je záměnnost pro: NAIL094

Anotace

čeština

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.

Poslední úprava: T_KTI (04.05.2012)

angličtina

A course on logic theories and procedures for deciding satisfiability in these theories with emphasis on the application in program verification. Construction of an efficient SAT solver (DPLL, conflict-directed clause learning), local algorithms for satisfiability (WalkSAT, survey propagation), decisions in logic with equality, uninterpreted functions and pointers, quantified Boolean formulae (QBF), combining logic theories, SAT-modulo solvers.

Poslední úprava: T_KTI (04.05.2012)

Cíl předmětu

čeština

Cílem předmětu je seznámit studenty se základními principy, které se používají při řešení SAT/SMT a souvisejících problémů

Poslední úprava: Kučera Petr, RNDr., Ph.D. (30.04.2020)

angličtina

The goal of the lecture is to introduce students with the basic principles and techniques used in SAT/SMT solving and related problems.

Poslední úprava: Kučera Petr, RNDr., Ph.D. (30.04.2020)

Podmínky zakončení předmětu

čeština

Předmět je zakončen zápočtem a zkouškou. K udělení zápočtu je třeba získat dostatečný počet bodů řešením domácích úkolů. Zkoušku je možné splnit dvěma způsoby. Jedním je ústní zkouška, která s ohledem na situaci může probíhat i distančně. Druhou možností je získání vyššího počtu bodů řešením domácích úkolů za podmínek, které jsou přesněji popsány na stránkách k předmětu (http://ktiml.mff.cuni.cz/~kucerap/satsmt/index-en.php)

Poslední úprava: Kučera Petr, RNDr., Ph.D. (30.04.2020)

angličtina

The course is finished with obtaining the credit and passing the exam. The credit is given for getting enough points for the homework assignments given during the semester. The exam can be passed in two ways. One possibility is to pass an oral exam which can proceed remotely depending on the current situation. The other option is to solve enough homework assignments, the conditions of this way of passing exam is described in more details at the course web pages (http://ktiml.mff.cuni.cz/~kucerap/satsmt/index-en.php)

Poslední úprava: Kučera Petr, RNDr., Ph.D. (30.04.2020)

Literatura

čeština

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.

Poslední úprava: T_KTI (04.05.2012)

Sylabus

čeština

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.

Přednáška je doplněna cvičením. Mimo klasických úloh na procvičení látky se

budou řešit také implementační úlohy pomocí existujících softwarových

knihoven.

Poslední úprava: T_KTI (04.05.2012)

angličtina

A course on logic theories and procedures for deciding satisfiability in

these theories with emphasis on the application in program verification.

Construction of an efficient SAT solver (DPLL, conflict-directed clause

learning), local algorithms for satisfiability (WalkSAT, survey

propagation), decisions in logic with equality, uninterpreted functions and

pointers, quantified Boolean formulae (QBF), combining logic theories,

SAT-modulo solvers.

The course is accompanied with a seminar. There will be tasks to exercise

the taught material as well as implementation tasks based on the existent

software libraries.

Poslední úprava: T_KTI (04.05.2012)