Abstrakt
Model checkovací nástroje založené na iterativní predikátové abstrakci (např. SLAM a BLAST) často používají specifikační jazyk pro vyjádření složitých pravidel chování.
Verifikované zdrojové kódy jsou obohaceny o umělé proměnné a příkazy s cílem převést problém ověření platnosti těchto pravidel na problém dosažitelnosti lokace v programu. Touto cestou jsou zdrojové kódy nafouknuty a během verifikace je nutné najít a sledovat další predikáty.
Znatelné zlepšení výkonu je možné dosáhnout sledováním stavu pravidel chování mimo/vedle samotných zdrojových kódů místo jejich instrumentace. Naimplementovali jsme rozšíření BLASTu, které přijímá specifikační jazyk (zjednodušená verze behavior protokolů) a ověří platnost bez modifikace vstupních zdrojových kódů.
Zlepšení výkonu je ukázáno na experimentu s dvěma Linux drivery.