Invention Grant
US08402440B2 Program verification through symbolic enumeration of control path programs
有权
通过对控制路径程序进行符号枚举的程序验证
- Patent Title: Program verification through symbolic enumeration of control path programs
- Patent Title (中): 通过对控制路径程序进行符号枚举的程序验证
-
Application No.: US12393500Application Date: 2009-02-26
-
Publication No.: US08402440B2Publication Date: 2013-03-19
- Inventor: Sriram Sankaranarayanan , Franjo Ivancic , William R Harris , Aarti Gupta , Gogul Balakrishnan
- Applicant: Sriram Sankaranarayanan , Franjo Ivancic , William R Harris , Aarti Gupta , Gogul Balakrishnan
- Applicant Address: US NJ Princeton
- Assignee: NEC Laboratories America, Inc.
- Current Assignee: NEC Laboratories America, Inc.
- Current Assignee Address: US NJ Princeton
- Agent Joseph Kolodka; Bao Tran
- Main IPC: G06F9/44
- IPC: G06F9/44
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.
Public/Granted literature
- US20100005454A1 PROGRAM VERIFICATION THROUGH SYMBOLIC ENUMERATION OF CONTROL PATH PROGRAMS Public/Granted day:2010-01-07
Information query
