Diagramy decyzyjne i model checking CTL

Prelegent(ci)

Tadeusz Sznuk

Afiliacja

Uniwersytet Warszawski

Termin

4 kwietnia 2011 10:15

Pokój

p. 4790

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

Zapewne nie wszystkie z poniższych tematów zdążę poruszyć, ale ogólny plan wygląda tak:
  * Diagramy decyzyjne (BDD):
      - Definicje, struktura
      - Operacje
      - Uwagi implementacyjne
      - Warianty
  * Model checking:
      - Definicje: modele, formuły itp.
      - Weryfikacja bezpośrednia
      - Weryfikacja symboliczna:
          - Za pomocą BDD
          - Za pomocą SAT-solvera.
      -  Zastosowania przy weryfikacji oprogramowania

---