Predicate Abstraction with Under-Approximation Refinement

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky Predikátová abstrakce a zjemňování dolních aproximací
Autoři

PELÁNEK Radek PASAREANU Corina VISSER Willem

Rok publikování 2007
Druh Článek v odborném periodiku
Časopis / Zdroj Logical Methods in Computer Science
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www LMCS journal web-page.
Obor Informatika
Klíčová slova model checking; predicate abstraction; under-approximation
Popis Navrhujeme metodu ověřování modelů založenou na abstrakci a zjemňování dolních aproximací. Metoda nevyžaduje generování abstraktních přechodů, místo toho prochází konkrétní přechody a pouze si ukládá abstraktní verze stavů specifikované abstrakčními predikáty. S využitím nástroje pro dokazování vět se automaticky kontroluje, zda při průchodu statového prostoru dochází ke ztrátě přesnosti. Aplikace metody je ilustrována na verifikaci souběžných programů.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.