V�b�rov� p�edn�ka o logick�ch teori�ch a procedur�ch rozhoduj�c� splnitelnost v t�chto teori�ch s d�razem na aplikaci p�i verifikaci program�. Na p�edn�ce se bude prob�rat: rozhodovac� procedury pro v�rokovou logiku (DPLL, BDD) logick� teorie pro rovnost, line�rn� aritmetiku, bitov� vektory, pole a ukazatele kombinov�n� rozhodovac�ch procedur, SMT ov��ov�n� korektnosti program�

P�edn�ka je dopln�na cvi�en�m. V r�mci cvi�en� bude mo�n� mimo klasick�ch �loh na procvi�en� l�tky �e�it tak� �lohy implementa�n�ho charakteru.

�mluva: mailem (ji� prob�hla).

Rozvrh: zimn� semestr, 2/2 Z+Zk, st�eda 12:20-13:50 S421 (p�en�ka) a 14:00-15:30 S421 (cvi�en�), Mal� Strana, (za��n� se 8.10.2014, S421 je chodba �FALu ve 4. pat�e)

Teaching in English: The lecture will be taught in English if required (study materials in English will be provided).

Plak�t p�edn�ky (reklama na �mluvu)    |   P�edn�ka v SISu