{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T07:03:39Z","timestamp":1725865419090},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319467498"},{"type":"electronic","value":"9783319467504"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-46750-4_1","type":"book-chapter","created":{"date-parts":[[2016,9,21]],"date-time":"2016-09-21T02:11:57Z","timestamp":1474423917000},"page":"3-24","source":"Crossref","is-referenced-by-count":10,"title":["Verification of Concurrent Programs on Weak Memory Models"],"prefix":"10.1007","author":[{"given":"Oleg","family":"Travkin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"key":"1_CR1","unstructured":"SV-Competition Benchmarks, April 2016. https:\/\/github.com\/dbeyer\/sv-benchmarks"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-662-46681-0_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2015","unstructured":"Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 353\u2013367. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_28"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-642-28756-5_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2012","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Counter-example guided fence insertion under TSO. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 204\u2013219. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28756-5_15"},{"key":"1_CR4","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). doi: 10.1007\/978-3-642-37036-6_28"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-39799-8_9","volume-title":"Computer Aided Verification","author":"J Alglave","year":"2013","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of\u00a0concurrent\u00a0software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 141\u2013157. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_9"},{"issue":"2","key":"1_CR6","doi-asserted-by":"crossref","first-page":"7:1","DOI":"10.1145\/2627752","volume":"36","author":"J Alglave","year":"2014","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 7:1\u20137:74 (2014)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Arora, N.S., Blumofe, R.D., Plaxton, C.G.: Thread scheduling for multiprogrammed multiprocessors. In: Proceedings of the Tenth Annual ACM Symposium on Parallel Algorithms and Architectures, SPAA 1998, pp. 119\u2013129. ACM, New York (1998)","DOI":"10.1145\/277651.277678"},{"key":"1_CR8","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). doi: 10.1007\/978-3-642-22110-1_9"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-662-46675-9_18","volume-title":"Fundamental Approaches to Software Engineering","author":"A Bouajjani","year":"2015","unstructured":"Bouajjani, A., Calin, G., Derevenetc, E., Meyer, R.: Lazy TSO reachability. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 267\u2013282. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46675-9_18"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Alur, R., Martin, M.M.K.: Checkfence: checking consistency of concurrent data types on relaxed memory models. In: Ferrante, J., McKinley, K.S. (eds.) Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, pp. 12\u201321. ACM (2007)","DOI":"10.1145\/1250734.1250737"},{"key":"1_CR11","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). doi: 10.1007\/978-3-540-70545-1_12"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/978-3-642-19835-9_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Burnim","year":"2011","unstructured":"Burnim, J., Sen, K., Stergiou, C.: Sound and complete monitoring of sequential consistency for relaxed memory models. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 11\u201325. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-19835-9_3"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Burnim, J., Sen, K., Stergiou, C.: Testing concurrent programs on relaxed memory models. In: Dwyer, M.B., Tip, F. (eds.) ISSTA 2011, pp. 122\u2013132. ACM (2011)","DOI":"10.1145\/2001420.2001436"},{"key":"1_CR14","unstructured":"Burns, J., Lynch, N.A.: Mutual exclusion using indivisible reads and writes. In: 18th Allerton Conference on Communication, Control, and Computing, pp. 833\u2013842 (1980)"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/978-3-642-14052-5_28","volume-title":"Interactive Theorem Proving","author":"E Cohen","year":"2010","unstructured":"Cohen, E., Schirmer, B.: From Total Store Order to Sequential Consistency: a practical reduction theorem. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 403\u2013418. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14052-5_28"},{"key":"1_CR16","unstructured":"I. Corporate SPARC International. The SPARC architecture manual: version 8. Prentice-Hall, Inc., Upper Saddle River, NJ, USA (1992)"},{"issue":"4","key":"1_CR17","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451\u2013490 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-15291-7_2","volume-title":"Euro-Par 2010 - Parallel Processing","author":"L Dalessandro","year":"2010","unstructured":"Dalessandro, L., Dice, D., Scott, M., Shavit, N., Spear, M.: Transactional mutex locks. In: D\u2019Ambra, P., Guarracino, M., Talia, D. (eds.) Euro-Par 2010. LNCS, vol. 6272, pp. 2\u201313. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15291-7_2"},{"key":"1_CR19","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). doi: 10.1007\/978-3-642-38856-9_7"},{"key":"1_CR20","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). doi: 10.1007\/978-3-662-46081-8_25"},{"key":"1_CR21","first-page":"43","volume-title":"Programming Languages: NATO Advanced Study Institute","author":"EW Dijkstra","year":"1968","unstructured":"Dijkstra, E.W.: Cooperating sequential processes. In: Genuys, F. (ed.) Programming Languages: NATO Advanced Study Institute, pp. 43\u2013112. Academic Press, New York (1968)"},{"issue":"6","key":"1_CR22","first-page":"1","volume":"17","author":"G Ernst","year":"2014","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV - overview and VerifyThis competition. Softw. Tools Techn. Transfer 17(6), 1\u201318 (2014)","journal-title":"Softw. Tools Techn. Transfer"},{"key":"1_CR23","volume-title":"The SPIN Model Checker - Primer and Reference Manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"key":"1_CR24","unstructured":"Intel, Santa Clara, CA, USA. Intel 64 and IA-32 Architectures Software Developer\u2019s Manual Volume 3A: System Programming Guide, Part 1, May 2012"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Inverso, O., Nguyen, T.L., Fischer, B., La Torre, S., Parlato, G.: Lazy-cseq: a context-bounded model checking tool for multi-threaded C-programs. In: Cohen, M.B., Grunske, L., Whalen, M. (eds.) 30th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA, pp. 807\u2013812. IEEE, 9\u201313 November 2015","DOI":"10.1109\/ASE.2015.108"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54862-8_26"},{"issue":"2","key":"1_CR27","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1145\/2261417.2261438","volume":"43","author":"M Kuperstein","year":"2012","unstructured":"Kuperstein, M., Vechev, M.T., Yahav, E.: Automatic inference of memory fences. SIGACT News 43(2), 108\u2013123 (2012)","journal-title":"SIGACT News"},{"issue":"8","key":"1_CR28","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"},{"issue":"9","key":"1_CR29","doi-asserted-by":"crossref","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis & transformation. In: 2nd IEEE\/ACM International Symposium on Code Generation and Optimization (CGO 2004), San Jose, CA, USA, pp. 75\u201388. IEEE Computer Society, 20\u201324 March 2004","DOI":"10.1109\/CGO.2004.1281665"},{"key":"1_CR31","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: Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 212\u2013226. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-16164-3_16"},{"key":"1_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-642-31424-7_36","volume-title":"Computer Aided Verification","author":"S Mador-Haim","year":"2012","unstructured":"Mador-Haim, S., Maranget, L., Sarkar, S., Memarian, K., Alglave, J., Owens, S., Alur, R., Martin, M.M.K., Sewell, P., Williams, D.: An axiomatic memory model for POWER multiprocessors. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 495\u2013512. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31424-7_36"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Meshman, Y., Rinetzky, N., Yahav, E.: Pattern-based synthesis of synchronization for the C++ memory model. In: Kaivola, R., Wahl, T. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, pp. 120\u2013127. IEEE, 27\u201330 September 2015","DOI":"10.1109\/FMCAD.2015.7542261"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","volume-title":"A Calculus of Communicating Systems","year":"1980","unstructured":"Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980)"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Park, S., Dill, D.L.: An executable specification, analyzer and verifier for RMO (Relaxed Memory Order). In: SPAA, pp. 34\u201341 (1995)","DOI":"10.1145\/215399.215413"},{"issue":"3","key":"1_CR36","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"G Peterson","year":"1981","unstructured":"Peterson, G.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115\u2013116 (1981)","journal-title":"Inf. Process. Lett."},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, pp. 46\u201357. IEEE Computer Society, 31 October\u20131 November 1977","DOI":"10.1109\/SFCS.1977.32"},{"issue":"7","key":"1_CR38","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1145\/1785414.1785443","volume":"53","author":"P Sewell","year":"2010","unstructured":"Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM 53(7), 89\u201397 (2010)","journal-title":"Commun. ACM"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Szymanski, B.K.: A simple solution to Lamport\u2019s concurrent programming problem with linear wait. In: Proceedings of the 2nd International Conference on Supercomputing, ICS 1988, pp. 621\u2013626. ACM, New York (1988)","DOI":"10.1145\/55364.55425"},{"key":"1_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-319-03077-7_21","volume-title":"Hardware and Software: Verification and Testing","author":"O Travkin","year":"2013","unstructured":"Travkin, O., M\u00fctze, A., Wehrheim, H.: SPIN as a linearizability checker under weak memory models. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 311\u2013326. Springer, Heidelberg (2013). doi: 10.1007\/978-3-319-03077-7_21"},{"key":"1_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-319-13338-6_11","volume-title":"Hardware and Software: Verification and Testing","author":"O Travkin","year":"2014","unstructured":"Travkin, O., Wehrheim, H.: Handling TSO in mechanized linearizability proofs. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 132\u2013147. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-13338-6_11"},{"key":"1_CR42","unstructured":"Treiber, R.K.: Systems programming: coping with parallelism. Technical report RJ 5118, IBM Almaden Res. Ctr. (1986)"},{"key":"1_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-319-26287-1_7","volume-title":"Hardware and Software: Verification and Testing","author":"H Wehrheim","year":"2015","unstructured":"Wehrheim, H., Travkin, O.: TSO to SC via symbolic execution. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 104\u2013119. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-26287-1_7"},{"issue":"5\u20136","key":"1_CR44","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1002\/cpe.837","volume":"17","author":"Y Yang","year":"2005","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G.: UMM: an operational memory model specification framework with integrated model checking capability. Concurrency Comput. Pract. Experience 17(5\u20136), 465\u2013487 (2005)","journal-title":"Concurrency Comput. Pract. Experience"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-46750-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,13]],"date-time":"2019-09-13T20:29:34Z","timestamp":1568406574000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46750-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319467498","9783319467504"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46750-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}