Karen Yorav: Modular model checking for sequential programs

 

Abstract: The main topic of my talk will be an algorithm that performs modular model checking on sequential programs. In contrast to hardware designs, the models of programs can be too large to fit into memory even when they consist of a single sequential unit. Furthermore, even when the model can be held in memory, model checking might exceed the memory capacity of the computer.

We present an algorithm that takes advantage of a partitioning of the text of a sequential program into subprograms, following the control flow structure. Each sub-program is translated into a Kripke structure, and this structure is kept in a separate file. The algorithm then performs CTL model checking while at any given point it only keeps one of these structures in the immediate memory of the computer.

The algorithm was implemented in a prototype tool and applied to a few small examples. In these example we have achieved reduction in both space and time requirements.

If time permits, I will present another part of my Ph.D. thesis, in which static analysis is used to reduce the size of the Kripke structure created for a given program.