next up previous
Next: Task 2.3: ESC/Java case Up: Task 2: Extended static Previous: Task 2.1: ESC/Java resource

Task 2.2: Resource annotation inference

Specifying resource consumption via annotations can be made more lightweight by inferring annotations automatically from unannotated codes. The Houdini [18] annotation assistant for ESC/Java is a productive verification tool which works in this way. We will investigate the use of Houdini for resource annotation inference.