Please use this identifier to cite or link to this item: https://scholarbank.nus.edu.sg/handle/10635/40488
DC FieldValue
dc.titleA type system for resource protocol verification and its correctness proof
dc.contributor.authorPopeea, C.
dc.contributor.authorChin, W.-N.
dc.date.accessioned2013-07-04T08:05:28Z
dc.date.available2013-07-04T08:05:28Z
dc.date.issued2004
dc.identifier.citationPopeea, 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.
dc.identifier.urihttp://scholarbank.nus.edu.sg/handle/10635/40488
dc.description.abstractWe 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.
dc.sourceScopus
dc.subjectCorrectness Proof
dc.subjectDependent Type System
dc.subjectPath-sensitive Analysis
dc.subjectProtocol Verification
dc.subjectResource Specification
dc.typeConference Paper
dc.contributor.departmentCOMPUTER SCIENCE
dc.description.sourcetitleProceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation
dc.description.page135-146
dc.identifier.isiutNOT_IN_WOS
Appears in Collections:Staff Publications

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

Page view(s)

125
checked on Nov 24, 2022

Google ScholarTM

Check


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