发明申请
- 专利标题： PROGRAM VERIFICATION THROUGH SYMBOLIC ENUMERATION OF CONTROL PATH PROGRAMS
- 专利标题（中）： 通过符号控制程序进行程序验证
-
申请号： US12393500申请日： 2009-02-26
-
公开(公告)号： US20100005454A1公开(公告)日： 2010-01-07
- 发明人: Sriram Sankaranarayanan , Aarti Gupta , William R. Harris , Gogul Balakrishnan , Franjo Ivancic
- 申请人： Sriram Sankaranarayanan , Aarti Gupta , William R. Harris , Gogul Balakrishnan , Franjo Ivancic
- 申请人地址： US NJ Princeton
- 专利权人： NEC LABORATORIES AMERICA, INC.
- 当前专利权人： NEC LABORATORIES AMERICA, INC.
- 当前专利权人地址： US NJ Princeton
- 主分类号： G06F11/36
- IPC分类号： G06F11/36
摘要：
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.
公开/授权文献
信息查询
