Patent Document ID: 20100305919
Application ID: 12753239
Patent Flag: 0

Claim One:
1. A method for symbolic model checking of sequential systems, comprising: 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.