===== Zadání =====
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í).

===== Vypracování =====
**Upozornění:** bez nároku na úplnost a korektnost. Podle hesla „lepší něco než nic“. Ale snaha byla o co nejlepší výsledek.

==== Abstraktní interpretace ====
  * metoda symbolického MC/statická analýza
  * místo nad skutečnými doménami proměnných se program interpretuje nad abstraktními

Jen pro úplnost:
  * abstraktní doména musí tvořit úplný svaz
  * místo každé instrukce definujeme monotónní funkci

An abstract interpretation I of a program P with n program locations is a tuple I = <L, ◦, ≤, T, ⊥, F> where (L, ≤) is a complete lattice, T and ⊥ are one and zero of (L, ≤), ◦ is equal either to [průsek nebo spojení] operation, and F is a monotone function on product lattice (Ln , ≤) defining the interpretation of basic instructions.

==== Metody abstrakce a aproximace ====

==== Redukce částečným uspořádáním ====
**Princip redukce:** Při generování grafů se místo funkce všech přímých následníků uvažuj pouze někteří přímí následníci vrcholu. V důsledku toho je počet vygenerovaných stavů produktového automatu menší.

**Technická realizace:** Optimální způsob výběru následníků je obtížný. Nástroje implementují různé heuristiky. Redukovaný stavový prostor musí zachovávat přítomnost akceptujícího cyklu. Formule nesmí obsahovat operátor X (podtřída LTL).

==== Metody zjemňování abstrakcí ====

=== CEGAR – protipříkladem řízené zjemňování abstrakcí ===
  * idea: verifikujeme overaproximovaný model systému – pokud splňuje specifikaci, v pořádku; pokud ne a nejde o falešný protipříklad, „OK“; jinak přidáme do abstrakce predikáty, které odpovídající chování odstraní (netriviální)
  * metoda ale nemusí nikdy skončit


===== Předměty =====
  * [[https://is.muni.cz/auth/predmet/fi/IA159|IA159 Formal Verification Methods]]

===== Související otázky =====
  * [[mgr-szz:in-tei:16-tei]] (kousek)

~~DISCUSSION~~