Model checking of non-terminating software programs
US7921411B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Oct 20, 2006 |
| Grant date | Apr 5, 2011 |
| Priority date | — |
| Expiry date | Feb 3, 2030 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F8/10
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method for verifying software program code includes specifying a property that the software program code is expected to satisfy. The software program code and the property are transformed into an initial logical formula in a static single assignment (SSA) form, the formula including variables. A loop in the software program code is identified. Successive over-approximations are applied to a portion of the initial logical formula corresponding to the loop in order to produce a modified logical formula in the SSA form that represents a finite over-approximation of a set of states that are reachable by the loop. It is verified that the software program code satisfies the specified property by determining whether there is an assignment of the variables that satisfies the modified logical formula.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.