{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T00:51:54Z","timestamp":1725670314426},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642286407"},{"type":"electronic","value":"9783642286414"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28641-4_4","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T17:10:46Z","timestamp":1332436246000},"page":"51-68","source":"Crossref","is-referenced-by-count":8,"title":["Parametric Verification of Address Space Separation"],"prefix":"10.1007","author":[{"given":"Jason","family":"Franklin","sequence":"first","affiliation":[]},{"given":"Sagar","family":"Chaki","sequence":"additional","affiliation":[]},{"given":"Anupam","family":"Datta","sequence":"additional","affiliation":[]},{"given":"Jonathan M.","family":"McCune","sequence":"additional","affiliation":[]},{"given":"Amit","family":"Vasudevan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"unstructured":"Alkassar, E., Cohen, E., Hillebrand, M., Kovalev, M., Paul, W.: Verifying shadow page table algorithms. In: Proceedings of FMCAD (2010)","key":"4_CR1"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-15057-9_3","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E. Alkassar","year":"2010","unstructured":"Alkassar, E., Hillebrand, M.A., Paul, W.J., Petrova, E.: Automated Verification of a Small Hypervisor. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol.\u00a06217, pp. 40\u201354. Springer, Heidelberg (2010)"},{"unstructured":"ARM Holdings: ARM1176JZF-S technical reference manual. Revision r0p7 (2009)","key":"4_CR3"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T. Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, Y., Zuck, L.: Parameterized Verification with Automatically Computed Inductive Assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 221\u2013234. Springer, Heidelberg (2001)"},{"doi-asserted-by":"crossref","unstructured":"Barham, P., Dragovic, B., Fraser, K., Hand, S., Harris, T., Ho, A., Neugebauer, R., Pratt, I., Warfield, A.: Xen and the art of virtualization. In: Proceedings of SOSP (2003)","key":"4_CR5","DOI":"10.1145\/945445.945462"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-21437-0_19","volume-title":"FM 2011: Formal Methods","author":"G. Barthe","year":"2011","unstructured":"Barthe, G., Betarte, G., Campo, J.D., Luna, C.: Formally Verifying Isolation and Availability in an Idealized Model of Virtualization. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 231\u2013245. Springer, Heidelberg (2011)"},{"doi-asserted-by":"crossref","unstructured":"Baumann, C., Blasum, H., Bormer, T., Tverdyshev, S.: Proving memory separation in a microkernel by code level verification. In: Proc. of AMICS (2011)","key":"4_CR7","DOI":"10.1109\/ISORCW.2011.14"},{"key":"4_CR8","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/10721959_19","volume-title":"Automated Deduction - CADE-17","author":"E.A. Emerson","year":"2000","unstructured":"Emerson, E.A., Kahlon, V.: Reducing Model Checking of the Many to the Few. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 236\u2013254. Springer, Heidelberg (2000)"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/3-540-46002-0_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.A. Emerson","year":"2002","unstructured":"Emerson, E.A., Kahlon, V.: Model Checking Large-Scale and Parameterized Resource Allocation Systems. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 251\u2013265. Springer, Heidelberg (2002)"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-540-39724-3_22","volume-title":"Correct Hardware Design and Verification Methods","author":"E.A. Emerson","year":"2003","unstructured":"Emerson, E.A., Kahlon, V.: Exact and Efficient Verification of Parameterized Cache Coherence Protocols. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 247\u2013262. Springer, Heidelberg (2003)"},{"doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Model checking guarded protocols. In: Proceedings of LICS (2003)","key":"4_CR12","DOI":"10.1109\/LICS.2003.1210076"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/3-540-36577-X_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.A. Emerson","year":"2003","unstructured":"Emerson, E.A., Kahlon, V.: Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 144\u2013159. Springer, Heidelberg (2003)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/3-540-61474-5_60","volume-title":"Computer Aided Verification","author":"E.A. Emerson","year":"1996","unstructured":"Emerson, E.A., Namjoshi, K.S.: Automatic Verification of Parameterized Synchronous Systems (Extended Abstract). In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 87\u201398. Springer, Heidelberg (1996)"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/BFb0028766","volume-title":"Computer Aided Verification","author":"E.A. Emerson","year":"1998","unstructured":"Emerson, E.A., Namjoshi, K.S.: Verification of Parameterized Bus Arbitration Protocol. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 452\u2013463. Springer, Heidelberg (1998)"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-24622-0_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Y. Fang","year":"2003","unstructured":"Fang, Y., Piterman, N., Pnueli, A., Zuck, L.: Liveness with Invisible Ranking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 223\u2013238. Springer, Heidelberg (2003)"},{"doi-asserted-by":"crossref","unstructured":"Franklin, J., Chaki, S., Datta, A., McCune, J.M., Vasudevan, A.: Parametric verification of address space separation. Tech. Rep. CMU-CyLab-12-001, CMU (2012)","key":"4_CR17","DOI":"10.1007\/978-3-642-28641-4_4"},{"doi-asserted-by":"crossref","unstructured":"Franklin, J., Chaki, S., Datta, A., Seshadri, A.: Scalable parametric verification of secure systems: How to verify reference monitors without worrying about data structure size. In: Proceedings of IEEE S&P (2010)","key":"4_CR18","DOI":"10.1109\/SP.2010.29"},{"issue":"3","key":"4_CR19","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S.M. German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. Journal of the ACM\u00a039(3), 675\u2013735 (1992)","journal-title":"Journal of the ACM"},{"doi-asserted-by":"crossref","unstructured":"Heitmeyer, C.L., Archer, M., Leonard, E.I., McLean, J.D.: Formal specification and verification of data separation in a separation kernel for an embedded system. In: Proceedings of ACM CCS (2006)","key":"4_CR20","DOI":"10.1145\/1180405.1180448"},{"unstructured":"Intel Corporation: Intel 64 and IA-32 Intel architecture software developer\u2019s manual. Intel Publication nos. 253665\u2013253669 (2008)","key":"4_CR21"},{"doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an os kernel. In: Proceedings of SOSP (2009)","key":"4_CR22","DOI":"10.1145\/1629575.1629596"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/11423348_17","volume-title":"Communicating Sequential Processes. The First 25 Years","author":"R. Lazi\u0107","year":"2005","unstructured":"Lazi\u0107, R., Newcomb, T., Roscoe, A.W.: On Model Checking Data-Independent Systems with Arrays with Whole-Array Operations. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) CSP 2004. LNCS, vol.\u00a03525, pp. 275\u2013291. Springer, Heidelberg (2005)"},{"doi-asserted-by":"crossref","unstructured":"Lazi\u0107, R., Newcomb, T., Roscoe, A.: On model checking data-independent systems with arrays without reset. Theory and Practice of Logic Programming 4(5&6) (2004)","key":"4_CR24","DOI":"10.1017\/S1471068404002054"},{"unstructured":"Neumann, P., Boyer, R., Feiertag, R., Levitt, K., Robinson, L.: A provably secure operating system: The system, its applications, and proofs. Tech. rep., SRI International (1980)","key":"4_CR25"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.D.: Automatic Deductive Verification with Invisible Invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, p. 82. Springer, Heidelberg (2001)"},{"doi-asserted-by":"crossref","unstructured":"Rushby, J.: The design and verification of secure systems. In: Proceedings of SOSP (1981) (ACM OS Review\u00a015(5))","key":"4_CR27","DOI":"10.1145\/800216.806586"},{"doi-asserted-by":"crossref","unstructured":"Shapiro, J.S., Weber, S.: Verifying the eros confinement mechanism. In: Proceedings of IEEE S&P (2000)","key":"4_CR28","DOI":"10.1109\/SECPRI.2000.848454"},{"issue":"2","key":"4_CR29","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1145\/358818.358825","volume":"23","author":"B.J. Walker","year":"1980","unstructured":"Walker, B.J., Kemmerer, R.A., Popek, G.J.: Specification and verification of the UCLA Unix security kernel. CACM\u00a023(2), 118\u2013131 (1980)","journal-title":"CACM"}],"container-title":["Lecture Notes in Computer Science","Principles of Security and Trust"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28641-4_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T22:02:33Z","timestamp":1606168953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28641-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642286407","9783642286414"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28641-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}