{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:48:18Z","timestamp":1725540498616},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642103728"},{"type":"electronic","value":"9783642103735"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10373-5_23","type":"book-chapter","created":{"date-parts":[[2009,11,16]],"date-time":"2009-11-16T06:45:27Z","timestamp":1258353927000},"page":"446-465","source":"Crossref","is-referenced-by-count":3,"title":["Combining Static Model Checking with Dynamic Enforcement Using the Statecall Policy Language"],"prefix":"10.1007","author":[{"given":"Anil","family":"Madhavapeddy","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","volume-title":"The SPIN Model Checker","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley, Reading (2003)"},{"key":"23_CR2","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1145\/1272996.1273009","volume-title":"EuroSys","author":"A. Madhavapeddy","year":"2007","unstructured":"Madhavapeddy, A., Ho, A., Deegan, T., Scott, D., Sohan, R.: Melange: creating a functional internet. In: Ferreira, P., Gross, T.R., Veiga, L. (eds.) EuroSys, pp. 101\u2013114. ACM, New York (2007)"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Ylonen, T., Lonvick, C.: The Secure Shell (SSH) Protocol Architecture. RFC 4251 (Proposed Standard) (January 2006)","DOI":"10.17487\/rfc4251"},{"key":"23_CR4","unstructured":"SDL: SDL forum society. Technical Report Recommendation Z.100, International Telecommunications Union, Geneva (1993)"},{"key":"23_CR5","unstructured":"ISO: Estelle\u2014a formal description technique based on an extended state transition model. ISO 9074, International Organisation for Standardization, Geneva (1997)"},{"key":"23_CR6","first-page":"396","volume-title":"Proceedings of the 10th International Conference on Software Engineering (ICSE)","author":"D. Harel","year":"1988","unstructured":"Harel, D., Lachover, H., Naamad, A., Pnueli, A., Politi, M., Sherman, R., Shtul-Trauring, A.: Statemate: a working environment for the development of complex reactive systems. In: Proceedings of the 10th International Conference on Software Engineering (ICSE), pp. 396\u2013406. IEEE Computer Society Press, Los Alamitos (1988)"},{"key":"23_CR7","doi-asserted-by":"crossref","first-page":"425","DOI":"10.7551\/mitpress\/5641.003.0021","volume-title":"The Foundations of Esterel: Proof, Language, and Interaction (Essay in Honor of Robin Milner)","author":"G. Berry","year":"2000","unstructured":"Berry, G.: III. In: The Foundations of Esterel: Proof, Language, and Interaction (Essay in Honor of Robin Milner), pp. 425\u2013454. MIT Press, Cambridge (2000)"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/3-540-45657-0_45","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 526\u2013538. Springer, Heidelberg (2002)"},{"key":"23_CR9","volume-title":"Programming in Occam","author":"G. Jones","year":"1986","unstructured":"Jones, G.: Programming in Occam. Prentice-Hall, Hertfordshire (1986)"},{"key":"23_CR10","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1145\/586110.586142","volume-title":"Proceedings of the 9th ACM Conference on Computer and Communications Security (CCS)","author":"H. Chen","year":"2002","unstructured":"Chen, H., Wagner, D.: MOPS: an infrastructure for examining security properties of software. In: Proceedings of the 9th ACM Conference on Computer and Communications Security (CCS), pp. 235\u2013244. ACM Press, New York (2002)"},{"issue":"11","key":"23_CR11","doi-asserted-by":"publisher","first-page":"1203","DOI":"10.1002\/1097-024X(200009)30:11<1203::AID-SPE338>3.0.CO;2-N","volume":"30","author":"E.R. Gansner","year":"2000","unstructured":"Gansner, E.R., North, S.C.: An open graph visualization system and its applications to software engineering. Software\u2014Practice and Experience\u00a030(11), 1203\u20131233 (2000)","journal-title":"Software\u2014Practice and Experience"},{"issue":"1","key":"23_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/366193.366201","volume":"6","author":"J.W. Backus","year":"1963","unstructured":"Backus, J.W., Bauer, F.L., Green, J., Katz, C., McCarthy, J., Perlis, A.J., Rutishauser, H., Samelson, K., Vauquois, B., Wegstein, J.H., van Wijngaarden, A., Woodger, M.: Revised report on the algorithm language ALGOL 60. Communications of the ACM\u00a06(1), 1\u201317 (1963)","journal-title":"Communications of the ACM"},{"key":"23_CR13","first-page":"2208","volume-title":"The Computer Science and Engineering Handbook","author":"L. Cardelli","year":"1997","unstructured":"Cardelli, L.: Type systems. In: Tucker, A.B. (ed.) The Computer Science and Engineering Handbook, pp. 2208\u20132236. CRC Press, Boca Raton (1997)"},{"issue":"1","key":"23_CR14","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"F.B. Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. ACM Transactions on Information Systems Security\u00a03(1), 30\u201350 (2000)","journal-title":"ACM Transactions on Information Systems Security"},{"key":"23_CR15","series-title":"Computer Science and Information Processing","volume-title":"Principles of Compiler Design","author":"A.V. Aho","year":"1977","unstructured":"Aho, A.V., Ullman, J.D.: Principles of Compiler Design. Computer Science and Information Processing. Addison-Wesley, Reading (1977)"},{"key":"23_CR16","unstructured":"Scott, D.J.: Abstracting Application-Level Security Policy for Ubiquitous Computing. PhD thesis, University of Cambridge (2005)"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"Ylonen, T., Lonvick, C.: The Secure Shell (SSH) Authentication Protocol. RFC 4252 (Proposed Standard) (January 2006)","DOI":"10.17487\/rfc4252"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Ylonen, T., Lonvick, C.: The Secure Shell (SSH) Connection Protocol. RFC 4254 (Proposed Standard) (January 2006)","DOI":"10.17487\/rfc4254"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/10722468_13","volume-title":"SPIN Model Checking and Software Verification","author":"J.C. Corbett","year":"2000","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J.: A language framework for expressing checkable properties of dynamic software. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 205\u2013223. Springer, Heidelberg (2000)"},{"issue":"1","key":"23_CR20","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/s100090200075","volume":"4","author":"J.C. Corbett","year":"2002","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Robby, Z.H.: Expressing checkable properties of dynamic systems: the Bandera Specification Language. International Journal on Software Tools for Technology Transfer\u00a04(1), 34\u201356 (2002)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"23_CR21","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1145\/337180.337234","volume-title":"Proceedings of the 22nd International Conference on Software Engineering (ICSE)","author":"J.C. Corbett","year":"2000","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C.S., Robby, Z.H.: Bandera: extracting finite-state models from Java source code. In: Proceedings of the 22nd International Conference on Software Engineering (ICSE), pp. 439\u2013448. ACM Press, New York (2000)"},{"key":"23_CR22","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Paris, France, pp. 106\u2013119. ACM Press, New York (1997)"},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-44585-4_15","volume-title":"Computer Aided Verification","author":"R. Alur","year":"2001","unstructured":"Alur, R., Wang, B.Y.: Verifying network protocol implementations by symbolic refinement checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 169\u2013181. Springer, Heidelberg (2001)"},{"key":"23_CR24","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/945445.945448","volume-title":"Proceedings of the Nineteenth ACM symposium on Operating Systems Principles","author":"R. Sekar","year":"2003","unstructured":"Sekar, R., Venkatakrishnan, V., Basu, S., Bhatkar, S., DuVarney, D.C.: Model-carrying code: a practical approach for safe execution of untrusted applications. In: Proceedings of the Nineteenth ACM symposium on Operating Systems Principles, pp. 15\u201328. ACM Press, New York (2003)"},{"key":"23_CR25","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1145\/586110.586145","volume-title":"Proceedings of the 9th ACM Conference on Computer and Communications Security (CCS)","author":"D. Wagner","year":"2002","unstructured":"Wagner, D., Soto, P.: Mimicry attacks on host-based intrusion detection systems. In: Atluri, V. (ed.) Proceedings of the 9th ACM Conference on Computer and Communications Security (CCS), pp. 255\u2013264. ACM, New York (2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10373-5_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,17]],"date-time":"2024-03-17T13:12:39Z","timestamp":1710681159000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10373-5_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642103728","9783642103735"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10373-5_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}