Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/40488
Title: A type system for resource protocol verification and its correctness proof
Authors: Popeea, C. 
Chin, W.-N. 
Keywords: Correctness Proof
Dependent Type System
Path-sensitive Analysis
Protocol Verification
Resource Specification
Issue Date: 2004
Source: Popeea, C.,Chin, W.-N. (2004). A type system for resource protocol verification and its correctness proof. Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation : 135-146. ScholarBank@NUS Repository.
Abstract: We present a new method, based on a form of dependent typing, to verify the correct usage of resources in a program. Our approach allows complex resources to be specified, whose properties are captured by annotated types and conditions on invariance and final states. The protocol itself is specified through a set of pre-defined methods, whose pre-condition and post-condition together, enforce the correct temporal usage of each resource type. We design a simple language together with a type system that shows how resource protocol verification can be achieved. We formalise an operational semantics for the language and provide a correctness proof which confirms that well-typed programs conform to the specified protocol of each resource type.
Source Title: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation
URI: http://scholarbank.nus.edu.sg/handle/10635/40488
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Page view(s)

51
checked on Dec 9, 2017

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.