Automatic region-based verification of garbage collectors

摘要

Systems and methods that add specifications to procedures in a garbage collector for indicating what each procedure does. Such annotations can be added in the source code, to indicate what the source code is to do when it runs—hence enabling an automatic verification of the garbage collector by a verification component. The specification can be presented as a logical formula that can be readily processed by a theorem prover, which is associated with the verification component. Such logical formulas can further employ regions to specify correctness of the garbage collector.

主权项

1. A computer implemented method comprising the following computer executable acts:
adding annotations via a specification in a source code of a garbage collector to indicate operation of the source during a run thereof; automatically generating verification conditions from each procedure of the source code based on the annotations; and automatically using a verification strategy based on regions for verifying the garbage collector by a verification component through the source code by automatically proving each verification condition without requiring the use of proof scripts.