发明授权
US08402440B2 Program verification through symbolic enumeration of control path programs
有权
通过对控制路径程序进行符号枚举的程序验证
- 专利标题： Program verification through symbolic enumeration of control path programs
- 专利标题（中）： 通过对控制路径程序进行符号枚举的程序验证
-
申请号： US12393500申请日： 2009-02-26
-
公开(公告)号： US08402440B2公开(公告)日： 2013-03-19
- 发明人: Sriram Sankaranarayanan , Franjo Ivancic , William R Harris , Aarti Gupta , Gogul Balakrishnan
- 申请人： Sriram Sankaranarayanan , Franjo Ivancic , William R Harris , Aarti Gupta , Gogul Balakrishnan
- 申请人地址： US NJ Princeton
- 专利权人： NEC Laboratories America, Inc.
- 当前专利权人： NEC Laboratories America, Inc.
- 当前专利权人地址： US NJ Princeton
- 代理商 Joseph Kolodka; Bao Tran
- 主分类号： G06F9/44
- IPC分类号： G06F9/44
摘要：
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.
公开/授权文献
信息查询
