Paralelní a distribuované systémy

1. Grafy a grafové algoritmy. Formalizace základních grafových pojmů, reprezentace grafů. Souvislost grafu, barevnost, rovinné grafy. Algoritmy (včetně složitosti a základní myšlenky důkazů korektnosti): prohledávání grafu do šířky a do hloubky, nejkratší vzdálenosti, kostry, toky v sítích.
   MA010, MA015
2. Matematická logika. Výroková a predikátová logika, syntaxe, sémantika. Odvozovací systémy, formální důkazy. Korektnost a úplnost odvozovacích systémů. Gödelovy věty o neúplnosti.
   MA007
3. Konečné automaty (FA) a logiky nad slovy. Logika 1.řádu (FOL) a monadická logika 2.řádu (MSOL): syntax a sémantika FOL a MSOL, principy převoditelnosti mezi FA a formulemi MSOL. Automaty nad nekonečnými slovy a omega-regulární jazyky.
   IA006
4. Operační, denotační, a axiomatická sémantika programovacích jazyků. CPO, věta o pevném bodě a její použití. Hoareova logika, její korektnost a úplnost. Temporální logiky  lineárního a větvícího se času a jejich fragmenty, sémantika neukončených a paralelních programů.
   IA011, IA040
5. Metoda ověřování modelu (MC) pro konečně stavové systémy a lineární temporální logiku. Princip překladu formulí LTL na automaty nad nekonečnými slovy.  Základní symbolické a explicitní algoritmy pro MC a jejich teoretická složitost.
   IA159
6. Formalismy pro modelování nekonečně stavových systémů (Petriho sítě, procesové přepisovací systémy, automaty, procesové kalkuly) a algebry procesů, porovnání jejich vyjadřovací síly vzhledem k bisimulaci. Vybrané rozhodnutelné problémy z oblasti verifikace těchto systémů.
   IA006, IA023
7. Specifické techniky pro verifikaci softwarových systémů, abstraktní interpretace, metody abstrakce a aproximace, redukce částečným uspořádáním, metody zjemňování abstrakcí (např. CEGAR – protipříkladem řízené zjemňování abstrakcí).
   IA159
8. Systémy reálného času. Měkké a tvrdé systémy. Plánování v systémech reálného času: plánování s periodickými úkoly, plánování založené na prioritách, přístup ke sdíleným zdrojům. 
   IA158
9. Modely distribuovaných systémů - základní pojmy a pricipy, synchronní a asynchronní komunikace. Synchronizace. Detekce ukončení.  Problém vzájemného vyloučení a problém uváznutí a jejich řešení.  Problém volby vedoucího prvku - vliv topologie a její znalosti/neznalosti na složitost řešení problému.
   IV100
10. Počítačové sítě - základní pojmy, principy, architektury. Spojované a nespojované sítě, OSI model, protokoly v prostředí Internetu. Směrování, základní služby počítačových sítí, správa a bezpečnost sítí.
    PA151 nebo PA159