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.
Jen pro úplnost:
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).