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

Download the presentation

Bob Kurshan

Bell Labs

Abstract

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.