You are in : Home » Results & submissions » Select UOA » 11 - Computer Science and Informatics » View submission: University of Edinburgh » Outputs » Detail

Output details

11 - Computer Science and Informatics

University of Edinburgh

Return to search Previous output Next output

Output 0 of 0 in the submission

Output title

Safety Guarantees from Explicit Resource Management

Type

E - Conference contribution

DOI

10.1007/978-3-540-92188-2_3

Name of conference/published proceedings

Formal Methods for Components and Objects

Volume number

Issue number

First page of article

ISSN of proceedings

0302-9743

Year of publication

2008

URL

http://link.springer.com/chapter/10.1007%2F978-3-540-92188-2_3

Number of additional authors

Additional information

<19> Originality: Presents a new language-based mechanism for managing complex usage patterns of external resources, with costly automated text messaging the motivating example. Previous mechanisms used runtime monitors; these new results remove instrumentation overhead by statically guaranteeing that code satisfies resource policies.

Significance: Part of the international "Mobius" collaboration using static analysis to provide "digital evidence" of security properties. Subsequent EC and EPSRC-funded projects (RESA, CerCo, AppGuarden) took up this idea of using formal methods to demonstrate resource safety in addition to functional correctness.

Rigour: Includes a detailed type-and-effect system, proven to correctly capture program resource usage at runtime.

Interdisciplinary

Cross-referral requested

Research group

F - Laboratory for Foundations of Computer Science

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract