Invention Grant
US07730455B2 Method and apparatus for enforcing safety properties of computer programs by generating and solving constraints
失效
通过生成和解决约束来实施计算机程序的安全属性的方法和装置
- Patent Title: Method and apparatus for enforcing safety properties of computer programs by generating and solving constraints
- Patent Title (中): 通过生成和解决约束来实施计算机程序的安全属性的方法和装置
-
Application No.: US11268802Application Date: 2005-11-07
-
Publication No.: US07730455B2Publication Date: 2010-06-01
- Inventor: Ajay Chander , Nayeem Islam , David Espinosa , Peter Lee , George Necula
- Applicant: Ajay Chander , Nayeem Islam , David Espinosa , Peter Lee , George Necula
- Applicant Address: JP Tokyo
- Assignee: NTT Docomo, Inc.
- Current Assignee: NTT Docomo, Inc.
- Current Assignee Address: JP Tokyo
- Agency: Blakely, Sokoloff, Taylor & Zafman LLP
- Main IPC: G06F9/44
- IPC: G06F9/44
Abstract:
A method and apparatus is disclosed herein for generating and solving constraints. In one embodiment, the method comprises modifying program code by inserting one or more dynamic annotations having unsolved variables, generating one or more constraints based on the one or more dynamic annotations using a verifier, solving the one or more generated constraints; and modifying the program code by inserting a dynamic annotation in place of an annotation containing an unsolved variable.
Public/Granted literature
Information query
