Patent · US Active

Program verification through symbolic enumeration of control path programs

US8402440B2 · kind B2 · utility

8Cited by

14References

26Claims

0Family size

Assignee

NEC Laboratories America, Inc. · US

Inventors

Sriram Sankaranarayanan · Plainsboro, US
Franjo Ivancic · Princeton, US
William R. Harris · Southfield, US
Aarti Gupta · Princeton, US
Gogul Balakrishnan · Plainsboro, US

Key dates

Filing date	Feb 26, 2009
Grant date	Mar 19, 2013
Priority date	—
Expiry date	Jan 20, 2032

Classification

Technology area (CPC G)Physics
CPC primaryG06F11/3608
WIPO fieldComputer technology
WIPO sectorElectrical engineering

Abstract

Systems and methods are disclosed to verify a program by symbolically enumerating path programs; verifying each path program to determine if the path program is correct or leads to a violation of a correctness property; determining a conflict set from the path program if the path program is proved correct; using the conflict set to avoid enumerating other related path programs that are also correct.

Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.