System and method for performing a path-sensitive verification on a program
US6938186B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | May 28, 2002 |
| Grant date | Aug 30, 2005 |
| Priority date | — |
| Expiry date | Jan 14, 2024 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F11/3608
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
Described is a method and system that performs path-sensitive verification on programs having any code base size. The method maintains a symbolic store that includes symbolic states. Each symbolic state includes a concrete state and an abstract state. The abstract state identifies a state in which the property being tested currently exists. The concrete state identifies other properties of the program. The symbolic store is updated at each node in a logic path of the program with changes in the abstract state and the concrete state. The updates occur such that the symbolic states associated with a particular edge of any node will not have identical abstract states. Rather, in this case, the symbolic states are merged by combining the concrete states to include content that is similar in both symbolic states. In addition, the concrete state determines relevant paths to proceed along in the logic path.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.