{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:08:15Z","timestamp":1725548895081},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540236351"},{"type":"electronic","value":"9783540376217"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-37621-7_6","type":"book-chapter","created":{"date-parts":[[2010,2,28]],"date-time":"2010-02-28T19:29:47Z","timestamp":1267385387000},"page":"113-133","source":"Crossref","is-referenced-by-count":0,"title":["Formal Specification and Verification of Resource Bound Security Using PVS"],"prefix":"10.1007","author":[{"given":"Weijiang","family":"Yu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aloysius K.","family":"Mok","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/3-540-45853-0_11","volume-title":"Computer Security - ESORICS 2002","author":"A.K. Mok","year":"2002","unstructured":"Mok, A.K., Yu, W.: TINMAN: A Resource Bound Security Checking System for Mobile Code. In: Gollmann, D., Karjoth, G., Waidner, M. (eds.) ESORICS 2002. LNCS, vol.\u00a02502, pp. 178\u2013193. Springer, Heidelberg (2002)"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-Carrying Code. In: ACM Symposium on Principles of Programming Languages, pp. 106\u2013119 (1997)","DOI":"10.1145\/263699.263712"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to Typed Assembly Language. In: ACM Symposium on Principles of Programming Languages, pp. 85\u201397 (1998)","DOI":"10.21236\/ADA358572"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Crary, K., Weirich, S.: Resource Bound Certification. In: The 27th Annual ACM Symposium on Principles of Programming Languages, pp. 184\u2013198 (2000)","DOI":"10.1145\/325694.325716"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/3-540-46425-5_11","volume-title":"Programming Languages and Systems","author":"M. Hofmann","year":"2000","unstructured":"Hofmann, M.: A Type System for Bounded Space and Functional In-Place Update\u2013Extended Abstract. In: Smolka, G. (ed.) ESOP 2000 and ETAPS 2000. LNCS, vol.\u00a01782, pp. 165\u2013179. Springer, Heidelberg (2000)"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Evans, N., Schneider, S.: Analysing Time Dependent Security Properties in CSP Using PVS. In: 6th European Symposium on Research in Computer Security, pp. 222\u2013237 (2000)","DOI":"10.1007\/10722599_14"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/3-540-58468-4_158","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"J. Hooman","year":"1994","unstructured":"Hooman, J.: Correctness of Real Time Systems by Construction. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol.\u00a0863, pp. 19\u201340. Springer, Heidelberg (1994)"},{"key":"6_CR8","series-title":"Lecture Notes in Artificial Intelligence","first-page":"748","volume-title":"11th International Conference on Automated Deduction","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J., Shankar, N.: PVS: A Prototype Verification System. In: 11th International Conference on Automated Deduction. LNCS (LNAI), pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Lee, P.: The Design and Implementation of a Certifying Compiler. In: Proceedings of the ACM Conference on Programming Language Design and Implementation, pp. 333\u2013344 (1998)","DOI":"10.1145\/277652.277752"},{"key":"6_CR10","unstructured":"Yu, W., Mok, A.K.: Enforcing Resource Bound Safety for Mobile SNMP Agents. In: 18th Annual Computer Security Applications Conference, pp. 69\u201377 (2002)"},{"key":"6_CR11","unstructured":"The Familiar Project, http:\/\/familiar.handhelds.org"}],"container-title":["Lecture Notes in Computer Science","Software Security - Theories and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-37621-7_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:40:55Z","timestamp":1605742855000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-37621-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540236351","9783540376217"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-37621-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}