UNICA IRIS Institutional Research Information System
IRIS è il sistema di gestione integrata dei dati della ricerca (persone, progetti, pubblicazioni, attività) adottato dall'Università degli Studi di Cagliari dal mese di luglio 2015.
EnglishAn 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.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo
| Titolo: | Local Policies for Resource Usage Analysis | |
| Autori: | ||
| Data di pubblicazione: | 2009 | |
| Rivista: | ||
| 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:
http://hdl.handle.net/11584/20345
Copyright © 2022