System and method for generating a predicate abstraction of a program
US7058925B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Apr 30, 2002 |
| Grant date | Jun 6, 2006 |
| Priority date | — |
| Expiry date | Feb 6, 2024 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F11/3608
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
Described is a method that enables the automatic generation of a boolean program that is a predicate abstraction of a program written using a general programming language. The method is capable of abstracting code statements within the program that include procedure calls, assignments, goto statements, conditionals, and pointers. In accordance with the invention, predicates of interest are identified for each code statement in the program. For each particular code statement, the process generates predicate statements that describe an effect that the statement has on the predicates of interest. If the effect of a particular code statement is indeterminable, non-deterministic predicate statements are included in the boolean program to model the indeterminable nature of the code statement. In addition, if a particular code statement includes a procedure call, the arguments and return value of the procedure call are translated to associated predicates in the calling context.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.