{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:56:01Z","timestamp":1725936961701},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319737201"},{"type":"electronic","value":"9783319737218"}],"license":[{"start":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T00:00:00Z","timestamp":1514505600000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-73721-8_3","type":"book-chapter","created":{"date-parts":[[2017,12,28]],"date-time":"2017-12-28T09:13:05Z","timestamp":1514452385000},"page":"47-70","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automatic Verification of RMA Programs via Abstraction Extrapolation"],"prefix":"10.1007","author":[{"given":"Cedric","family":"Baumann","sequence":"first","affiliation":[]},{"given":"Andrei Marian","family":"Dan","sequence":"additional","affiliation":[]},{"given":"Yuri","family":"Meshman","sequence":"additional","affiliation":[]},{"given":"Torsten","family":"Hoefler","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Vechev","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,12,29]]},"reference":[{"key":"3_CR1","unstructured":"Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: The benefits of duality in verifying concurrent programs under TSO. In: Desharnais, J., Jagadeesan, R. (eds.) 27th International Conference on Concurrency Theory, CONCUR 2016, Qu\u00e9bec City, Canada, August 23\u201326, 2016. LIPIcs, vol. 59, pp. 5:1\u20135:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-642-33125-1_13","volume-title":"Static Analysis","author":"PA Abdulla","year":"2012","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Automatic fence insertion in integer programs via predicate abstraction. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 164\u2013180. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33125-1_13"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Alglave, J., Cousot, P.: Ogre and pythia: an invariance proof method for weak consistency models. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18\u201320, 2017, pp. 3\u201318. ACM (2017)","DOI":"10.1145\/3009837.3009883"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1007\/978-3-319-08867-9_33","volume-title":"Computer Aided Verification","author":"J Alglave","year":"2014","unstructured":"Alglave, J., Kroening, D., Nimal, V., Poetzl, D.: Don\u2019t sit on the fence: a static analysis approach to automatic fence insertion. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 508\u2013524. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_33"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-642-37036-6_28","volume-title":"Programming Languages and Systems","author":"J Alglave","year":"2013","unstructured":"Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 512\u2013532. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_28"},{"issue":"2","key":"3_CR6","doi-asserted-by":"crossref","first-page":"310","DOI":"10.1147\/sj.402.0310","volume":"40","author":"F Allen","year":"2001","unstructured":"Allen, F., Almasi, G., Andreoni, W., Beece, D., Berne, B.J., Bright, A., Brunheroto, J., Cascaval, C., Castanos, J., Coteus, P., Crumley, P., Curioni, A., Denneau, M., Donath, W., Eleftheriou, M., Fitch, B., Fleischer, B., Georgiou, C.J., Germain, R., Giampapa, M., Gresh, D., Gupta, M., Haring, R., Ho, H., Hochschild, P., Hummel, S., Jonas, T., Lieber, D., Martyna, G., Maturu, K., Moreira, J., Newns, D., Newton, M., Philhower, R., Picunko, T., Pitera, J., Pitman, M., Rand, R., Royyuru, A., Salapura, V., Sanomiya, A., Shah, R., Sham, Y., Singh, S., Snir, M., Suits, F., Swetz, R., Swope, W.C., Vishnumurthy, N., Ward, T.J.C., Warren, H., Zhou, R.: Blue Gene: A vision for protein science using a petaflop supercomputer. IBM Syst. J. 40(2), 310\u2013327 (2001)","journal-title":"IBM Syst. J."},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Alverson, R., Roweth, D., Kaplan, L.: The Gemini system interconnect. In: Proc. of the IEEE Symposium on High Performance Interconnects (HOTI 2010), pp. 83\u201387. IEEE Computer Society (2010)","DOI":"10.1109\/HOTI.2010.23"},{"key":"3_CR8","unstructured":"Andrews, G.R.: Concurrent programming - principles and practice. Benjamin\/Cummings (1991)"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Arimilli, B., Arimilli, R., Chung, V., Clark, S., Denzel, W., Drerup, B., Hoefler, T., Joyner, J., Lewis, J., Li, J., Ni, N., Rajamony, R.: The PERCS high-performance interconnect. In: Proc. of the IEEE Symposium on High Performance Interconnects (HOTI 2010), pp. 75\u201382. IEEE Computer Society, August 2010","DOI":"10.1109\/HOTI.2010.16"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-22110-1_9","volume-title":"Computer Aided Verification","author":"MF Atig","year":"2011","unstructured":"Atig, M.F., Bouajjani, A., Parlato, G.: Getting rid of store-buffers in TSO analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 99\u2013115. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_9"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Burke, M., Soffa, M.L. (eds.) Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Snowbird, Utah, USA, June 20\u201322, 2001, pp. 203\u2013213. ACM (2001)","DOI":"10.1145\/378795.378846"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Barrett, B.W., Brightwell, R.B., Pedretti, K.T.T., Wheeler, K.B., Hemmert, K.S., Riesen, R.E., Underwood, K.D., Maccabe, A.B., Hudson, T.B. :The Portals 4.0 network programming interface. Tech. rep., Sandia National Laboratories, SAND2012-10087 (2012)","DOI":"10.2172\/1088065"},{"key":"3_CR13","unstructured":"Beck, M., Kagan, M.: Performance evaluation of the RDMA over Ethernet (RoCE) standard in enterprise data centers infrastructure. In: Proc. of the Workshop on Data Center - Converged and Virtual Ethernet Switching (DC-CaVES 2011), pp. 9\u201315. ITCP (2011)"},{"key":"3_CR14","unstructured":"Jeannet, B.: The ConcurInterproc Analyzer, September 2017. http:\/\/pop-art.inrialpes.fr\/interproc\/concurinterprocweb.cgi"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-642-37036-6_29","volume-title":"Programming Languages and Systems","author":"A Bouajjani","year":"2013","unstructured":"Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 533\u2013553. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_29"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-70545-1_12","volume-title":"Computer Aided Verification","author":"S Burckhardt","year":"2008","unstructured":"Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 107\u2013120. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_12"},{"key":"3_CR17","unstructured":"Calin, G., Derevenetc, E., Majumdar, R., Meyer, R.: A theory of partitioned global address spaces. In: Seth, A., Vishnoi, N.K. (eds.) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2013, Guwahati, India, December 12\u201314, 2013. LIPIcs, vol. 24, pp. 127\u2013139. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)"},{"key":"3_CR18","unstructured":"Cray Inc., Using the GNI and DMAPP APIs. Ver. S-2446-52, March 2014. http:\/\/docs.cray.com\/"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Dan, A.M., Lam, P., Hoefler, T., Vechev, M.T.: Modeling and analysis of remote memory access programming. In: Visser, E., Smaragdakis, Y. (eds.) Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 \u2013 November 4, 2016, pp. 129\u2013144. ACM (2016)","DOI":"10.1145\/2983990.2984033"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-38856-9_7","volume-title":"Static Analysis","author":"AM Dan","year":"2013","unstructured":"Dan, A.M., Meshman, Y., Vechev, M., Yahav, E.: Predicate abstraction for relaxed memory models. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 84\u2013104. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_7"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-662-46081-8_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Dan","year":"2015","unstructured":"Dan, A., Meshman, Y., Vechev, M., Yahav, E.: Effective abstractions for verification under relaxed memory models. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 449\u2013466. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46081-8_25"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"3_CR23","unstructured":"Dijkstra, E.: Cooperating sequential processes, TR EWD-123. Tech. rep., Technological University, Eindhoven (1965)"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Donaldson, A.F., Kaiser, A., Kroening, D., Wahl, T.: Symmetry-aware predicate abstraction for shared-variable concurrent programs. In: Gopalakrishnan and Qadeer [27], pp. 356\u2013371","DOI":"10.1007\/978-3-642-22110-1_28"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Faanes, G., Bataineh, A., Roweth, D., Court, T., Froese, E., Alverson, B., Johnson, T., Kopnick, J., Higgins, M., Reinhard, J.: Cray cascade: a scalable HPC system based on a dragonfly network. In: Proc. of the International Conference for High Performance Computing, Networking, Storage and Analysis (SC 2012), pp. 103:1\u2013103:9. IEEE Computer Society (2012)","DOI":"10.1109\/SC.2012.39"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Gerstenberger, R., Besta, M., Hoefler, T.: Enabling highly-scalable remote memory access programming with MPI-3 one sided. In: Proc. of the ACM\/IEEE Supercomputing, SC 2013, pp. 53:1\u201353:12 (2013)","DOI":"10.1145\/2503210.2503286"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","first-page":"457","volume-title":"Computer Aided Verification","year":"2011","unstructured":"Gopalakrishnan, G., Qadeer, S. (eds.): CAV 2011. LNCS, vol. 6806, pp. 457\u2013462. Springer, Heidelberg (2011)"},{"key":"3_CR28","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., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: Ball, T., Sagiv, M. (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26\u201328, 2011 (2011), pp. 331\u2013344. ACM","DOI":"10.1145\/1926385.1926424"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Threader: a constraint-based verifier for multi-threaded programs. In: Gopalakrishnan and Qadeer [27], pp. 412\u2013417","DOI":"10.1007\/978-3-642-22110-1_32"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Hoefler, T., Dinan, J., Thakur, R., Barrett, B., Balaji, P., Gropp, W., Underwood, K.: Remote Memory Access Programming in MPI-3. ACM Transactions on Parallel Computing (TOPC), January 2015","DOI":"10.1145\/2780584"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Islam, N.S., Rahman, M.W., Jose, J., Rajachandrasekar, R., Wang, H., Subramoni, H., Murthy, C., Panda, D.K.: High performance RDMA-based design of HDFS over InfiniBand. In: Proceedings of the International Conference on High Performance Computing, Networking, Storage and Analysis (Los Alamitos, CA, USA, 2012), SC 2012, pp. 35:1\u201335:35. IEEE Computer Society Press (2012)","DOI":"10.1109\/SC.2012.65"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Kuperstein, M., Vechev, M.T., Yahav, E.: Partial-coherence abstractions for relaxed memory models. In: Hall, M.W., Padua, D.A. (eds.) Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4\u20138, 2011, pp. 187\u2013198. ACM (2011)","DOI":"10.1145\/1993498.1993521"},{"issue":"8","key":"3_CR34","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L Lamport","year":"1974","unstructured":"Lamport, L.: A new solution of Dijkstra\u2019s concurrent programming problem. Commun. ACM 17(8), 453\u2013455 (1974)","journal-title":"Commun. ACM"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-642-16164-3_16","volume-title":"Model Checking Software","author":"A Linden","year":"2010","unstructured":"Linden, A., Wolper, P.: An automata-based symbolic approach for verifying programs on relaxed memory models. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 212\u2013226. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16164-3_16"},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-319-10936-7_15","volume-title":"Static Analysis","author":"Y Meshman","year":"2014","unstructured":"Meshman, Y., Dan, A., Vechev, M., Yahav, E.: Synthesis of memory fences via refinement propagation. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 237\u2013252. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10936-7_15"},{"key":"3_CR37","unstructured":"OpenFabrics Alliance (OFA). OpenFabrics Enterprise Distribution (OFED) (2014). www.openfabrics.org"},{"issue":"3","key":"3_CR38","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"GL Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115\u2013116 (1981)","journal-title":"Inf. Process. Lett."},{"key":"3_CR39","unstructured":"de Le\u00f3n, H.P., Furbach, F., Heljanko, K., Meyer, R.: Portability analysis for axiomatic memory models. PORTHOS: one tool for all models. CoRR abs\/1702.06704 (2017)"},{"key":"3_CR40","doi-asserted-by":"crossref","unstructured":"Recio, R., Metzler, B., Culley, P., Hilland, J., Garcia, D.: A Remote Direct Memory Access Protocol Specification. RFC 5040, RFC Editor, October 2007","DOI":"10.17487\/rfc5040"},{"key":"3_CR41","doi-asserted-by":"crossref","unstructured":"Schmid, P., Besta, M., Hoefler, T.: High-performance distributed RMA locks. In: Proceedings of the 25th Symposium on High-Performance Parallel and Distributed Computing (HPDC 2016), June 2016","DOI":"10.1145\/2907294.2907323"},{"key":"3_CR42","doi-asserted-by":"crossref","unstructured":"Szymanski, B.K.: A simple solution to lamport\u2019s concurrent programming problem with linear wait. In: International Conference on Supercomputing, pp. 621\u2013626 (1988)","DOI":"10.1145\/55364.55425"},{"key":"3_CR43","unstructured":"The InfiniBand Trade Association. Infiniband Architecture Spec, vol. 1, Rel. 1.2. InfiniBand Trade Association (2004)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-73721-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T20:00:48Z","timestamp":1570564848000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-73721-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,29]]},"ISBN":["9783319737201","9783319737218"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-73721-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017,12,29]]}}}