Verification of a program partitioned according to the control flow information of the program
US8171438B2 · kind B2 · utility
Assignee
Inventor
Key dates
| Filing date | Aug 25, 2006 |
| Grant date | May 1, 2012 |
| Priority date | — |
| Expiry date | Feb 16, 2031 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F8/433
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
Provided are a method, system, and article of manufacture for verification of a program partitioned according to the control flow information of the program. Properties are received indicating outcome states for a program. The program is processed to determine a control flow in the program and paths in the control flow. Enabled paths are determined in the control flow having states satisfying requirements of the outcome states. For each enabled path, a determination is made of inert variables not used along the control flow of the path and a representation of states and transitions for the enabled path is generated, wherein the represented states and transitions do not include the inert variables. The generated representation of the states and transitions for the enabled path are combined into a merged computation image.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.