Method and apparatus for finding errors in software programs using satisfiability of constraints
US7089542B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Dec 13, 2002 |
| Grant date | Aug 8, 2006 |
| Priority date | — |
| Expiry date | Oct 11, 2024 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F11/3608
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method and apparatus are provided for analyzing software programs. The invention combines data flow analysis and symbolic execution with a new constraint solver to create a more efficient and accurate static software analysis tool. The disclosed constraint solver combines rewrite rules with arithmetic constraint solving to provide a constraint solver that is efficient, flexible and capable of satisfactorily expressing semantics and handling arithmetic constraints. The disclosed constraint solver comprises a number of data structures to remember existing range, equivalence and inequality constraints and incrementally add new constraints. The constraint solver returns an inconsistent indication only if the range constraints, equivalence constraints, and inequality constraints are mutually inconsistent.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.