Automatically abstracting a model relative to the property being
checked has become a core algorithm in commercial model-checking
tools. In it's simplest form, it merely computes the cone of influence
of the property. It is possible to do much better though.
I will describe the localization reduction algorithm in the tool
FormalCheck. It tries to avoid data paths, and inessential blocks
within the cone of influence. As a result, it can verify and/or
falsify significantly larger models than cone of influence reduction
alone.
|
