An extension of the λ-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, that is, a sound overapproximation to the set of histories obtainable at runtime. After a suitable transfor- mation, history expressions are model-checked for validity. A program is resource-safe if its history expression is verified valid: If such, no runtime monitor is needed to safely drive its executions.
Local Policies for Resource Usage Analysis
BARTOLETTI, MASSIMO;DEGANO, PIERPAOLO;FERRARI, GIAN-LUIGI;FERRARI, GIAN-LUIGI
2009-01-01
Abstract
An extension of the λ-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, that is, a sound overapproximation to the set of histories obtainable at runtime. After a suitable transfor- mation, history expressions are model-checked for validity. A program is resource-safe if its history expression is verified valid: If such, no runtime monitor is needed to safely drive its executions.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
