Method and apparatus for enforcing safety properties of computer programs by generating and solving constraints
First Claim
Patent Images
1. A method comprising:
- 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.
2 Assignments
0 Petitions
Accused Products
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.
24 Citations
28 Claims
-
1. A method comprising:
-
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. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9, 13, 14)
-
-
10. An article of manufacture having one or more recordable media storing instructions thereon which, when executed by a system, cause the system to perform a method comprising:
-
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. - View Dependent Claims (11, 12)
-
-
15. An apparatus comprising:
-
a memory; and
a processor coupled to a memory, to execute instructions stored in the memory to perform a method comprising 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.
-
-
16. A method comprising:
-
evaluating resource usage of computer program code; and
annotating the computer program, by inserting one or more operations into the computer program code for resource use safety, based on a result of evaluating the resource usage of the computer program code. - View Dependent Claims (17, 18, 19, 20, 21)
-
-
22. An article of manufacture having one or more recordable media storing instructions thereon which, when executed by a system, cause the system to perform a method comprising:
-
evaluating resource usage of computer program code; and
annotating the computer program, by inserting one or more operations into the computer program code for resource use safety, based on a result of evaluating the resource usage of the computer program code. - View Dependent Claims (23, 24, 25, 26, 27)
-
-
28. An apparatus comprising:
-
a memory; and
a processor coupled to a memory, to execute instructions stored in the memory to perform a method comprising evaluating resource usage of computer program code; and
annotating the computer program, by inserting one or more operations into the computer program code for resource use safety, based on a result of evaluating the resource usage of the computer program code.
-
Specification