METHOD AND APPARATUS FOR ENFORCING SAFETY PROPERTIES OF COMPUTER PROGRAMS BY GENERATING AND SOLVING CONSTRAINTS
摘要
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.
申请公布号
WO2006053103(A2)
申请公布日期
2006.05.18
申请号
WO2005US40690
申请日期
2005.11.08
申请人
NTT DOCOMO INC.;CHANDER, AJAY;ISLAM, NAYEEM;ESPINOSA, DAVID;LEE, PETER;NECULA, GEORGE
发明人
CHANDER, AJAY;ISLAM, NAYEEM;ESPINOSA, DAVID;LEE, PETER;NECULA, GEORGE