{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:46:33Z","timestamp":1742913993458,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661964"},{"type":"electronic","value":"9783319661971"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66197-1_12","type":"book-chapter","created":{"date-parts":[[2017,8,11]],"date-time":"2017-08-11T21:02:30Z","timestamp":1502485350000},"page":"185-202","source":"Crossref","is-referenced-by-count":4,"title":["Using Shared Memory Abstractions to Design Eager Sequentializations for Weak Memory\u00a0Models"],"prefix":"10.1007","author":[{"given":"Ermenegildo","family":"Tomasco","sequence":"first","affiliation":[]},{"given":"Truc Lam","family":"Nguyen","sequence":"additional","affiliation":[]},{"given":"Bernd","family":"Fischer","sequence":"additional","affiliation":[]},{"given":"Salvatore","family":"La\u00a0Torre","sequence":"additional","affiliation":[]},{"given":"Gennaro","family":"Parlato","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,13]]},"reference":[{"key":"12_CR1","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":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-662-54580-5_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2017","unstructured":"Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: Context-bounded analysis for POWER. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 56\u201374. Springer, Heidelberg (2017). doi: 10.1007\/978-3-662-54580-5_4"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Abe, T., Maeda, T.: A general model checking framework for various memory consistency models. In: IEEE PDP, pp. 332\u2013341 (2014)","DOI":"10.1109\/IPDPSW.2014.47"},{"key":"12_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":"12_CR5","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-39799-8_9","volume-title":"Computer Aided Verification","author":"Jade Alglave","year":"2013","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: CAV, pp. 141\u2013157 (2013)"},{"issue":"2","key":"12_CR6","doi-asserted-by":"publisher","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":"12_CR7","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":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"887","DOI":"10.1007\/978-3-662-49674-9_55","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2016","unstructured":"Beyer, D.: Reliable and reproducible competition results with BenchExec and witnesses (Report on SV-COMP 2016). In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 887\u2013904. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49674-9_55"},{"key":"12_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":"12_CR10","doi-asserted-by":"crossref","unstructured":"Carter, M., He, S., Whitaker, J., Rakamaric, Z., Emmi, M.: SMACK software verification toolchain. In: ICSE, pp. 589\u2013592 (2016)","DOI":"10.1145\/2889160.2889163"},{"issue":"6","key":"12_CR11","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1109\/TDSC.2013.25","volume":"10","author":"G Chen","year":"2013","unstructured":"Chen, G., Jin, H., Zou, D., Zhou, B.B., Liang, Z., Zheng, W., Shi, X.: Safestack: automatically patching stack-based buffer overflow vulnerabilities. IEEE Trans. Dependable Sec. Comput. 10(6), 368\u2013379 (2013)","journal-title":"IEEE Trans. Dependable Sec. Comput."},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-319-19195-9_2","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"A Horn","year":"2015","unstructured":"Horn, A., Kroening, D.: On partial order semantics for SAT\/SMT-based symbolic encodings of weak memory concurrency. In: Graf, S., Viswanathan, M. (eds.) FORTE 2015. LNCS, vol. 9039, pp. 19\u201334. Springer, Cham (2015). doi: 10.1007\/978-3-319-19195-9_2"},{"key":"12_CR13","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: ASE, pp. 807\u2013812 (2015)","DOI":"10.1109\/ASE.2015.108"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-319-08867-9_39","volume-title":"Computer Aided Verification","author":"O Inverso","year":"2014","unstructured":"Inverso, O., Tomasco, E., Fischer, B., La Torre, S., Parlato, G.: Bounded model checking of multi-threaded C programs via lazy sequentialization. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 585\u2013602. Springer, Cham (2014). doi: 10.1007\/978-3-319-08867-9_39"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Model-checking parameterized concurrent programs using linear interfaces. In: CAV, pp. 629\u2013644 (2010)","DOI":"10.1007\/978-3-642-14295-6_54"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Sequentializing Parameterized Programs. In: FIT, pp. 34\u201347 (2012)","DOI":"10.4204\/EPTCS.87.4"},{"issue":"1","key":"12_CR17","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10703-009-0078-9","volume":"35","author":"A Lal","year":"2009","unstructured":"Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods Syst. Des. 35(1), 73\u201397 (2009)","journal-title":"Formal Methods Syst. Des."},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-642-03359-9_27","volume-title":"Theorem Proving in Higher Order Logics","author":"S Owens","year":"2009","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 391\u2013407. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-03359-9_27"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93\u2013107. Springer, Heidelberg (2005). doi: 10.1007\/978-3-540-31980-1_7"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Thomson, P., Donaldson, A.F., Betts, A.: Concurrency testing using schedule bounding: an empirical study. In: PPopp, pp. 15\u201328 (2014)","DOI":"10.1145\/2555243.2555260"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/978-3-662-46681-0_52","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Tomasco","year":"2015","unstructured":"Tomasco, E., Inverso, O., Fischer, B., La Torre, S., Parlato, G.: Verifying concurrent programs by memory unwinding. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 551\u2013565. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_52"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Tomasco, E., Nguyen, T.L., Inverso, O., Fischer, B., La Torre, S., Parlato, G.: Lazy sequentialization for TSO and PSO via shared memory abstractions. In: FMCAD, pp. 193\u2013200 (2016)","DOI":"10.1109\/FMCAD.2016.7886679"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"938","DOI":"10.1007\/978-3-662-49674-9_65","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Tomasco","year":"2016","unstructured":"Tomasco, E., Nguyen, T.L., Inverso, O., Fischer, B., La Torre, S., Parlato, G.: MU-CSeq 0.4: individual memory location unwindings. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 938\u2013941. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49674-9_65"},{"key":"12_CR24","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, Cham (2015). doi: 10.1007\/978-3-319-26287-1_7"},{"issue":"6","key":"12_CR25","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1145\/2813885.2737956","volume":"50","author":"Naling Zhang","year":"2015","unstructured":"Zhang, N., Kusano, M., Wang, C.: Dynamic partial order reduction for relaxed memory models. In: PLDI, pp. 250\u2013259 (2015)","journal-title":"ACM SIGPLAN Notices"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"Zheng, M., Rogers, M.S., Luo, Z., Dwyer, M.B., Siegel, S.F.: CIVL: formal verification of parallel programs. In: ASE, pp. 830\u2013835 (2015)","DOI":"10.1109\/ASE.2015.99"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66197-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T06:03:05Z","timestamp":1569996185000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66197-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661964","9783319661971"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66197-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}