Please use this identifier to cite or link to this item: https://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
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.

Google ScholarTM

Check


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