{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:07:27Z","timestamp":1776305247528,"version":"3.50.1"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319216676","type":"print"},{"value":"9783319216683","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21668-3_9","type":"book-chapter","created":{"date-parts":[[2015,7,13]],"date-time":"2015-07-13T15:08:53Z","timestamp":1436800133000},"page":"144-160","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Verifying Linearizability of Intel\u00ae Software Guard Extensions"],"prefix":"10.1007","author":[{"given":"Rebekah","family":"Leslie-Hurd","sequence":"first","affiliation":[]},{"given":"Dror","family":"Caspi","sequence":"additional","affiliation":[]},{"given":"Matthew","family":"Fernandez","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,14]]},"reference":[{"key":"9_CR1","unstructured":"Baumann, A., Peinado, M., Hunt, G.: Shielding applications from an untrusted cloud with Haven. In: 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014. USENIX Advanced Computing Systems Association, October 2014"},{"key":"9_CR2","unstructured":"Bensalem, S., Ganesh, V., Lakhnech, Y., Mu\u00f1oz, C., Owre, S., Rue\u00df, H., Rushby, J., Rusu, V., Sa\u00efdi, H., Shankar, N., Singerman, E., Tiwari, A.: An overview of SAL. In: LFM, pp. 187\u2013196, Williamsburg, VA, USA (2000)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Bingham, B., Bingham, J., Paula, F.M.d., Erickson, J., Singh, G., Reitblatt, M.: Industrial strength distributed explicit state model checking. In: PDMC, pp. 28\u201336, Washington, DC, USA (2010)","DOI":"10.1109\/PDMC-HiBi.2010.13"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174\u2013177. Springer, Heidelberg (2009)"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a complete and automatic linearizability checker. In: Programming Language Design and Implementation, PLDI 2010, June 2010","DOI":"10.1145\/1806596.1806634"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/978-3-642-14295-6_41","volume-title":"Computer Aided Verification","author":"P \u010cern\u00fd","year":"2010","unstructured":"\u010cern\u00fd, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., Alur, R.: Model checking of linearizability of concurrent list implementations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 465\u2013479. Springer, Heidelberg (2010)"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: ICCD, pp. 522\u2013525, Cambridge, MA, USA (1992)","DOI":"10.1109\/ICCD.1992.276232"},{"key":"9_CR8","unstructured":"Erk\u00f6k, L.: SBV: SMT based verification in Haskell. http:\/\/leventerkok.github.io\/sbv\/"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-24732-6_18","volume-title":"Model Checking Software","author":"C Flanagan","year":"2004","unstructured":"Flanagan, C.: Verifying commit-atomicity using model-checking. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 252\u2013266. Springer, Heidelberg (2004)"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Fraer, R., Keren, D., Khasidashvili, Z., Novakovsky, A., Puder, A., Singerman, E., Talmor, E., Vardi, M., Yang, J.: From visual to logic formalisms for SoC validation. In: Formal Methods and Models for System Design, MEMOCODE 2014","DOI":"10.1109\/MEMCOD.2014.6961855"},{"issue":"4","key":"9_CR11","doi-asserted-by":"crossref","first-page":"3030","DOI":"10.1145\/2611429.2617811","volume":"12","author":"A Gill","year":"2014","unstructured":"Gill, A.: Domain-specific languages and code synthesis using Haskell. Queue 12(4), 3030\u20133043 (2014)","journal-title":"Queue"},{"key":"9_CR12","unstructured":"Gill, A., Bull, T., Farmer, A., Kimmell, G., Komp, E.: Types and associated type families for hardware simulation and synthesis: the internals and externals of Kansas lava. In: Higher-Order and Symbolic Computation, pp. 1\u201320 (2013)"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Goel, A., Krsti\u0107, S., Leslie, R., Tuttle, M.R.: SMT-based system verification with DVF. In: Satisfiability Modulo Theories, SMT 2012, pp. 32\u201343 (2012)","DOI":"10.29007\/59rn"},{"issue":"3","key":"9_CR14","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"MP Herlihy","year":"1990","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. (TOPLAS) 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Hoekstra, M., Lal, R., Pappachan, P., Phegade, V., Del Cuvillo, J.: Using innovative instructions to create trustworthy software solutions. In: Proceedings of the 2nd International Workshop on Hardware and Architectural Support for Security and Privacy, HASP 2013, ACM, New York, NY, USA (2013)","DOI":"10.1145\/2487726.2488370"},{"key":"9_CR16","unstructured":"Intel Corporation, Santa Clara, CA, USA. $${\\rm Intel}\\textregistered $$ 64 and IA-32 Architectures Software Developer\u2019s Manual, September 2014"},{"key":"9_CR17","unstructured":"Intel Corporation, Santa Clara, CA, USA. $${\\rm Intel}\\textregistered $$ Software Guard Extensions Programming Reference, October 2014"},{"key":"9_CR18","unstructured":"Marlow, S.: Haskell 2010 language report 2010"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Matthews, J., Cook, B., Launchbury, J.: Microprocessor specification in Hawk. In: Proceedings of the 1998 International Conference on Computer Languages, pp. 90\u2013101. IEEE Computer Society Press (1998)","DOI":"10.1109\/ICCL.1998.674160"},{"key":"9_CR20","unstructured":"Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: Eigth Symposium on Operating Systems Design and Implementation, OSDI 2008. USENIX, December 2008"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-16612-9_26","volume-title":"Runtime Verification","author":"L Pike","year":"2010","unstructured":"Pike, L., Goodloe, A., Morisset, R., Niller, S.: Copilot: a hard real-time runtime monitor. 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. 6418, pp. 345\u2013359. Springer, Heidelberg (2010)"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-642-39176-7_20","volume-title":"Model Checking Software","author":"D Sethi","year":"2013","unstructured":"Sethi, D., Talupur, M., Malik, S.: Model checking unbounded concurrent lists. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 320\u2013340. Springer, Heidelberg (2013)"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-642-14295-6_40","volume-title":"Computer Aided Verification","author":"V Vafeiadis","year":"2010","unstructured":"Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 450\u2013464. Springer, Heidelberg (2010)"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-642-02652-2_21","volume-title":"Model Checking Software","author":"M Vechev","year":"2009","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Experience with model checking linearizability. In: P\u0103s\u0103reanu, C.S. (ed.) Model Checking Software. LNCS, vol. 5578, pp. 261\u2013278. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21668-3_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T04:46:35Z","timestamp":1748493995000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21668-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216676","9783319216683"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21668-3_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"14 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}