Predicate abstraction via symbolic decision procedures
US7587707B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Jul 1, 2005 |
| Grant date | Sep 8, 2009 |
| Priority date | — |
| Expiry date | May 11, 2026 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F11/3692
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
Predicate abstraction techniques and tools. Using symbolic decision procedures, predicate abstractions for computer programs are generated based on a set of predicates representing observations of expected behavior of the program. The set of predicates may be generated by an automatic program analysis tool or may be provided a user based on the user's observations. The predicate abstraction process may employ binary decision diagrams. Two or more symbolic decision procedures (e.g., for different kinds of program logic) can be combined to form a combined symbolic decision procedure to be used for predicate abstraction. A data structure can be used to track derived predicates during predicate abstraction.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.