Case-reduced verification condition generation system and method using weakest precondition operator expressed using strongest postcondition operators
US6553362B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Jul 16, 2001 |
| Grant date | Apr 22, 2003 |
| Priority date | — |
| Expiry date | Jul 16, 2021 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F9/44589
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
The instructions in a computer program are converted into a form of weakest precondition so as to produce a verification condition that is to be evaluated by a theorem prover. In generating the weakest precondition, labels are introduced for values of variables at control join points. In two preferred embodiments, the computer program is converted into a set of guarded commands prior to the application of weakest precondition operators. In one embodiment, as part of the process of generating the verification condition, assignment commands that assign values to variables are removed from the program through use of a “dynamic single assumption” technique. In another embodiment, the weakest precondition is expressed in terms of strongest postconditions. In both embodiments, a simplified verification condition is produced in which duplications of sets of instructions following a choice operator is avoided.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.