{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T13:22:08Z","timestamp":1760016128830},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642314230"},{"type":"electronic","value":"9783642314247"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_39","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T10:26:49Z","timestamp":1340274409000},"page":"548-563","source":"Crossref","is-referenced-by-count":9,"title":["Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement"],"prefix":"10.1007","author":[{"given":"Matthew","family":"Fredrikson","sequence":"first","affiliation":[]},{"given":"Richard","family":"Joiner","sequence":"additional","affiliation":[]},{"given":"Somesh","family":"Jha","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[]},{"given":"Phillip","family":"Porras","sequence":"additional","affiliation":[]},{"given":"Hassen","family":"Sa\u00efdi","sequence":"additional","affiliation":[]},{"given":"Vinod","family":"Yegneswaran","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"39_CR1","doi-asserted-by":"crossref","unstructured":"Aktug, I., Naliuka, K.: Conspec \u2013 a formal language for policy specification. ENTCS\u00a0197 (February 2008)","DOI":"10.1016\/j.entcs.2007.10.013"},{"key":"39_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Adding nesting structure to words. JACM\u00a056(3) (2009)","DOI":"10.1145\/1516512.1516518"},{"key":"39_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL (2002)","DOI":"10.1145\/503272.503274"},{"key":"39_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-642-16612-9_15","volume-title":"Runtime Verification","author":"E. Bodden","year":"2010","unstructured":"Bodden, E., Lam, P., Hendren, L.: Clara: A Framework for Partially Evaluating Finite-State Runtime Monitors Ahead of Time. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol.\u00a06418, pp. 183\u2013197. Springer, Heidelberg (2010)"},{"key":"39_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/978-3-540-31980-1_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Chen","year":"2005","unstructured":"Chen, F., Ro\u015fu, G.: Java-MOP: A Monitoring Oriented Programming Environment for Java. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 546\u2013550. Springer, Heidelberg (2005)"},{"key":"39_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. JACM\u00a050(5) (2003)","DOI":"10.1145\/876638.876643"},{"key":"39_CR7","unstructured":"Crockford, D.: Adsafe: Making JavaScript safe for advertising, \n                    \n                      http:\/\/www.adsafe.org"},{"key":"39_CR8","doi-asserted-by":"crossref","unstructured":"Erlingsson, \u00da., Schneider, F.B.: SASI enforcement of security policies: a retrospective. In: NSPW (2000)","DOI":"10.1145\/335169.335201"},{"key":"39_CR9","unstructured":"Evans, D., Twyman, A.: Flexible policy-directed code safety. In: SP (1999)"},{"key":"39_CR10","unstructured":"Facebook, Inc. FBJS, \n                    \n                      http:\/\/wiki.developers.facebook.com\/index.php\/FBJS"},{"key":"39_CR11","unstructured":"Google inc. The Caja project, \n                    \n                      http:\/\/code.google.com\/p\/google-caja\/"},{"key":"39_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"39_CR13","unstructured":"Guarnieri, S., Livshits, B.: Gatekeeper: Mostly static enforcement of security and reliability policies for JavaScript code. In: Security (August 2009)"},{"key":"39_CR14","doi-asserted-by":"crossref","unstructured":"Hamlen, K.W., Jones, M.: Aspect-oriented in-lined reference monitors. In: PLAS (2008)","DOI":"10.1145\/1375696.1375699"},{"key":"39_CR15","doi-asserted-by":"crossref","unstructured":"Hamlen, K.W., Morrisett, G., Schneider, F.B.: Certified in-lined reference monitoring on .NET. In: PLAS (2006)","DOI":"10.1145\/1134744.1134748"},{"key":"39_CR16","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL (2002)","DOI":"10.1145\/503272.503279"},{"key":"39_CR17","unstructured":"G. Inc. Closure Compiler, \n                    \n                      http:\/\/code.google.com\/closure\/compiler\/"},{"key":"39_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/3-540-45337-7_18","volume-title":"ECOOP 2001 - Object-Oriented Programming","author":"G. Kiczales","year":"2001","unstructured":"Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An Overview of AspectJ. In: Lindskov Knudsen, J. (ed.) ECOOP 2001. LNCS, vol.\u00a02072, pp. 327\u2013353. Springer, Heidelberg (2001)"},{"key":"39_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/BFb0053381","volume-title":"ECOOP \u201997 - Object-Oriented Programming","author":"G. Kiczales","year":"1997","unstructured":"Kiczales, G., Lamping, J., Mendhekar, A., Maeda, C., Lopes, C., Marc Loingtier, J., Irwin, J.: Aspect-Oriented Programming. In: Aksit, M., Auletta, V. (eds.) ECOOP 1997. LNCS, vol.\u00a01241, pp. 220\u2013242. Springer, Heidelberg (1997)"},{"key":"39_CR20","unstructured":"Kiefer, S., Schwoon, S., Suwimonteerabuth, D.: Moped: A model checker for pushdown systems, \n                    \n                      http:\/\/www.fmi.uni-stuttgart.de\/szs\/tools\/moped\/"},{"key":"39_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-540-89330-1_22","volume-title":"Programming Languages and Systems","author":"S. Maffeis","year":"2008","unstructured":"Maffeis, S., Mitchell, J.C., Taly, A.: An Operational Semantics for JavaScript. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol.\u00a05356, pp. 307\u2013325. Springer, Heidelberg (2008)"},{"key":"39_CR22","doi-asserted-by":"crossref","unstructured":"Maffeis, S., Taly, A.: Language-based isolation of untrusted Javascript. In: CSF (2009)","DOI":"10.1109\/CSF.2009.11"},{"key":"39_CR23","doi-asserted-by":"crossref","unstructured":"Maffeis, S., Taly, J.M.A.: Language-based isolation of untrusted JavaScript. In: SP (2010)","DOI":"10.1109\/CSF.2009.11"},{"key":"39_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-540-87403-4_5","volume-title":"Recent Advances in Intrusion Detection","author":"L. Martignoni","year":"2008","unstructured":"Martignoni, L., Stinson, E., Fredrikson, M., Jha, S., Mitchell, J.C.: A Layered Architecture for Detecting Malicious Behaviors. In: Lippmann, R., Kirda, E., Trachtenberg, A. (eds.) RAID 2008. LNCS, vol.\u00a05230, pp. 78\u201397. Springer, Heidelberg (2008)"},{"key":"39_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-31980-1_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2005","unstructured":"McMillan, K.L.: Applications of Craig Interpolants in Model Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 1\u201312. Springer, Heidelberg (2005)"},{"key":"39_CR26","doi-asserted-by":"crossref","unstructured":"Meyerovich, L., Livshits, B.: Conscript: Specifying and enforcing fine-grained security policies for javascript in the browser. In: SP (2010)","DOI":"10.1109\/SP.2010.36"},{"key":"39_CR27","doi-asserted-by":"crossref","unstructured":"Saxena, P., Akhawe, D., Hanna, S., McCamant, S., Mao, F., Song, D.: A symbolic execution framework for JavaScript. In: SP (2010)","DOI":"10.1109\/SP.2010.38"},{"key":"39_CR28","doi-asserted-by":"crossref","unstructured":"Schneider, F.B.: Enforceable security policies. TISSEC\u00a03 (February 2000)","DOI":"10.1145\/353323.353382"},{"key":"39_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-642-11319-2_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M. Sridhar","year":"2010","unstructured":"Sridhar, M., Hamlen, K.W.: Model-Checking In-Lined Reference Monitors. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 312\u2013327. Springer, Heidelberg (2010)"},{"key":"39_CR30","doi-asserted-by":"crossref","unstructured":"Yu, D., Chander, A., Islam, N., Serikov, I.: JavaScript instrumentation for browser security. In: POPL (2007)","DOI":"10.1145\/1190216.1190252"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31424-7_39.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:59:58Z","timestamp":1620115198000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}