Method and apparatus for statically analyzing a computer program for data dependencies
US5987252A · kind A · utility
Assignee
Inventors
Key dates
| Filing date | Sep 19, 1997 |
| Grant date | Nov 16, 1999 |
| Priority date | — |
| Expiry date | Sep 19, 2017 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06N5/013
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method and an apparatus analyze a computer program for dependencies of the program output on the program input. To analyze the program, the program is transformed by a function into a Boolean expression called a verification condition. An example of this function is the weakest liberal precondition. The verification condition characterizes a condition between the input and the output of the program that must be satisfied for the output to be independent of the input. A theorem prover evaluates the verification condition to determine whether the output would depend on the input if the program was executed. If the verification condition evaluates to true, then the output is independent of the input; false, then the output depends on the input.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.