System and method for model checking by interleaving stateless and state-based methods

A computer readable storage medium comprising a computer readable program for symbolic model checking of sequential systems, wherein the computer readable program when executed on a computer causes the computer to perform the steps of:

• alternating between state-based and state-less symbolic model checking methods, stored on computer readable storage media, by:
• performing symbolic state traversal (ST) to compute and store new frontier states in successive steps of the state-based method, wherein each step includes:
• building transition relations between successive sequential depths using control flow reachability information of the system;
• and
• performing image computations using the transition relations from the frontier states computed in previous steps to obtain image states, wherein the frontier states include a set of states reachable at a depth d from initial states;
• and
• performing bounded model checking (BMC) in the state-less method to check reachability of given goal states from the frontier states along paths of bounded length by building and unrolling the transition relations using control flow reachability information, without computing or storing intermediate reachable states.

A system for symbolic model checking of sequential systems, comprising:

• a model checking program stored in on a memory device and, when executed by a processor, alternates between state-based and state-less symbolic model checking methods;
• the model checking program including a state-based module configured to perform symbolic state traversal (ST) to compute and store new frontier states in successive steps by building transition relations between successive sequential depths using control flow reachability information of the system and performing image computations using the transition relations from the frontier states computed in previous steps to obtain image states, wherein the frontier states include a set of states reachable at a depth d from initial states;
• and
• the model checking program including a stateless module configured to perform bounded model checking (BMC) to check reachability of given goal states from the frontier states along paths of bounded length by building and unrolling the transition relations using control flow reachability information, without computing or storing intermediate reachable states.