System and method for model checking by interleaving stateless and state-based methods
US8589126B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Apr 2, 2010 |
| Grant date | Nov 19, 2013 |
| Priority date | — |
| Expiry date | Sep 19, 2032 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F11/3608
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method for symbolic model checking for sequential systems using a combination of state-based and state-less approaches. A state-based method is used to compute frontier states by building transition relations on-the-fly using control flow information of the system, and performing successive image computations until a memory bound is reached, and efficiently storing only the new frontier states as disjunctive partitions of Boolean and Arithmetic expressions. A stateless method is used to check reachability of given goal states from a heuristically chosen set of frontier states until depth/time bound is reached. These two methods are alternated until one of the following occurs: all frontier states are explored, all goal states are reached, all computing resources are exhausted. Even though we do not store the entire reachable state set, we guarantee a complete coverage for terminating programs without the need to compute a fixed-point.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.