An extension of the lambda-calculus is proposed, to study resource usage analysis and verification. It features usage policies with a possibly nested, local scope, and dynamic creation of resources. We define a type and effect system that, given a program, extracts a history expression, i.e. a sound over-approximation to the set of histories obtainable at run-time. After a suitable transformation, history expressions are model-checked for validity. A program is resource-safe if its history expression is verified valid: if such, no run-time monitor is needed to safely drive its executions.
Local Policies for Resource Usage Analysis
BARTOLETTI, MASSIMO;
2009-01-01
Abstract
An extension of the lambda-calculus is proposed, to study resource usage analysis and verification. It features usage policies with a possibly nested, local scope, and dynamic creation of resources. We define a type and effect system that, given a program, extracts a history expression, i.e. a sound over-approximation to the set of histories obtainable at run-time. After a suitable transformation, history expressions are model-checked for validity. A program is resource-safe if its history expression is verified valid: if such, no run-time monitor is needed to safely drive its executions.
I metadati presenti in IRIS UNICA sono rilasciati con licenza Creative Commons CC0 1.0 Universal, mentre i file delle pubblicazioni sono protetti da diritto d'autore, salvo diversa indicazione.
