Predicate Abstraction with Under-Approximation Refinement

Varování

Publikace nespadá pod Ústav výpočetní techniky, 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:	Institut Teoretické Informatiky Automatická analýza modelů pomocí procházení stavového prostoru