Memory consumption policies using Hoare logic

Memory consumption policies provide a means to control resource usage on constrained devices, and play an important role in ensuring the overall quality of software systems, and in particular resistance against resource exhaustion attacks. Such memory consumption policies have been previously enforced through static analyses, which yield automatic bounds at the cost of precision, or run-time analyses, which incur an overhead that is not acceptable for constrained devices.

In this talk, we present a static and precise verification technique based on Hoare style logic for guaranteeing bounded memory consumption for Java bytecode programs.