Local Policies for Resource Usage Analysis

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 M; PIERPAOLO DEGANO; GIAN LUIGI FERRARI; ROBERTO ZUNINO. - In: ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS. - ISSN 0164-0925. - 31(2009), pp. 1-43.

Trovami (UniCASearch)


Titolo: Local Policies for Resource Usage Analysis
Autori: 
BARTOLETTI, MASSIMO
mostra contributor esterni 
Data di pubblicazione: 2009
Rivista: 
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS  
Citazione: Local Policies for Resource Usage Analysis / BARTOLETTI M; PIERPAOLO DEGANO; GIAN LUIGI FERRARI; ROBERTO ZUNINO. - In: ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS. - ISSN 0164-0925. - 31(2009), pp. 1-43.
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.
Handle: http://hdl.handle.net/11584/20345
Tipologia:1.1 Articolo in rivista

File in questo prodotto:
Non ci sono file associati a questo prodotto.
Utilizza questo identificativo per citare o creare un link a questo documento:
http://hdl.handle.net/11584/20345
  • Citazioni
  • ND

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
 
 
 
Powered by IRIS-about IRIS-Utilizzo dei cookie
Logo CINECA  Copyright © 2020