Symbolic depth-first searches using control flow information for improved reachability analysis
US8271253B2 · kind B2 · utility
Assignee
Inventor
Key dates
| Filing date | Mar 16, 2007 |
| Grant date | Sep 18, 2012 |
| Priority date | — |
| Expiry date | Aug 29, 2030 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
Methods are provided for performing depth-first searches of concrete models of systems using control flow information of the system for improved reachability analysis. The concrete model's control structure and dependencies are extracted and an over-approximated (conservative) abstract control model is created. The abstract control model simulates the concrete model during model checking. Model checking the abstract control model produces execution traces based on the control paths of the concrete model. These execution traces may be used to guide a state space search on the concrete model during invariant checking to determine satisability of one or more selected invariants of the system.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.