Please use this identifier to cite or link to this item:
|Title:||A type system for resource protocol verification and its correctness proof||Authors:||Popeea, C.
Dependent Type System
|Issue Date:||2004||Citation:||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.
checked on Sep 22, 2022
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.