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í).

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

• 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.

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).

• 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

• IA159 Formal Verification Methods

• 16-tei (kousek)