Browse Prior Art Database

Using control flow analysis to improve the performance of rules in a model checker

IP.com Disclosure Number: IPCOM000016030D
Original Publication Date: 2002-Oct-29
Included in the Prior Art Database: 2003-Jun-21

Publishing Venue

IBM

Abstract

Problem The main problem in running rules in a model checker is referred to as the state explosion problem. Execution time is usually exponentially related to the program size. For a certain class of rules, it is possible to use control flow analysis to reduce the program size on which the rule is performed. Solution This invention represents a means for reducing the program size using control flow analysis, prior to executing the rule on the program with the model checker. We use the idea of dominating blocks to figure out which blocks are not relevant for our rules, and we remove these blocks from the program.