IBM Logo
IBM Research Lab in Haifa
Hot Shots  
FV Research in HRL  

Download the presentation

Bob Kurshan

Bell Labs


The Localization Reduction

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.