{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T20:51:05Z","timestamp":1742935865780,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031223365"},{"type":"electronic","value":"9783031223372"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-22337-2_24","type":"book-chapter","created":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T10:08:41Z","timestamp":1672222121000},"page":"494-510","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Consistency and\u00a0Persistency in\u00a0Program Verification: Challenges and\u00a0Opportunities"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[]},{"given":"Ahmed","family":"Bouajjani","sequence":"additional","affiliation":[]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[]},{"given":"K. Narayan","family":"Kumar","sequence":"additional","affiliation":[]},{"given":"Prakash","family":"Saivasan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,12,29]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Bouajjani, A., Kumar, K.N., Saivasan, P.: Deciding reachability under persistent x86-tso. In: Proceedings of the ACM on Programming Languages, vol. 5, no. POPL, pp. 1\u201332 (2021)","DOI":"10.1145\/3434337"},{"key":"24_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). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_4"},{"key":"24_CR3","unstructured":"Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: A load-buffer semantics for total store ordering. Log. Methods Comput. Sci. 14(1), 9 (2018)"},{"key":"24_CR4","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27\u201330 1996, pp. 313\u2013321. IEEE Computer Society (1996)"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Deneux, J., Mahata, P.: Multi-clock timed networks. In: 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14\u201317 July 2004, Turku, Finland, Proceedings, pp. 345\u2013354. IEEE Computer Society (2004)","DOI":"10.1109\/LICS.2004.1319629"},{"key":"24_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-540-78163-9_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"PA Abdulla","year":"2008","unstructured":"Abdulla, P.A., Ben Henda, N., Delzanno, G., Rezine, A.: Handling parameterized systems with non-atomic global conditions. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 22\u201336. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78163-9_7"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. In: Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS 1993), Montreal, Canada, 19\u201323 June 1993, pp. 160\u2013170. IEEE Computer Society (1993)","DOI":"10.1109\/LICS.1993.287591"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/BFb0028760","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"1998","unstructured":"Abdulla, P.A., Jonsson, B., Kindahl, M., Peled, D.: A general approach to partial order reductions in symbolic verification. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 379\u2013390. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028760"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: Hermenegildo, M.V., Palsberg, J., (eds.), Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, 17\u201323 Jan 2010, pp. 7\u201318. ACM (2010)","DOI":"10.1145\/1707801.1706303"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-28869-2_2","volume-title":"Programming Languages and Systems","author":"MF Atig","year":"2012","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: What\u2019s decidable about weak memory models? In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 26\u201346. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_2"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Parlato, G.: Context-bounded analysis of TSO systems. In: From Programs to Systems. The Systems perspective in Computing - ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, 6 Apr 2014. Proceedings, pp. 21\u201338 (2014)","DOI":"10.1007\/978-3-642-54848-2_2"},{"key":"24_CR12","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"},{"issue":"1\u20132","key":"24_CR13","first-page":"1","volume":"1","author":"S Burckhardt","year":"2014","unstructured":"Burckhardt, S.: Principles of eventual consistency. Found. Trends Program. Lang. 1(1\u20132), 1\u2013150 (2014)","journal-title":"Found. Trends Program. Lang."},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-662-43951-7_14","volume-title":"Automata, Languages, and Programming","author":"E Derevenetc","year":"2014","unstructured":"Derevenetc, E., Meyer, R.: Robustness against Power is PSpace-complete. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014. LNCS, vol. 8573, pp. 158\u2013170. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43951-7_14"},{"issue":"1\u20132","key":"24_CR15","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1\u20132), 63\u201392 (2001)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"24_CR16","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1145\/564585.564601","volume":"33","author":"S Gilbert","year":"2002","unstructured":"Gilbert, S., Lynch, N.A.: Brewer\u2019s conjecture and the feasibility of consistent, available, partition-tolerant web services. SIGACT News 33(2), 51\u201359 (2002)","journal-title":"SIGACT News"},{"key":"24_CR17","unstructured":"Intel. Architectures software developer\u2019s manual (combined volumes) Software.intel.com (2019)"},{"key":"24_CR18","unstructured":"Intel. Intel Optane Technology (2019). www.intel.com\/content\/www\/us\/en\/architecture-and-technology\/intel-optane-technology.html"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Lahav, O., Boker, U.: Decidable verification under a causally consistent shared memory. In: Donaldson, A.F., Torlak, E., (eds.) Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, 15\u201320 June 2020, pp. 211\u2013226. ACM (2020)","DOI":"10.1145\/3385412.3385966"},{"key":"24_CR20","doi-asserted-by":"crossref","unstructured":"Lahav, O., Giannarakis, N., Vafeiadis, V.: Taming release-acquire consistency. In: Bod\u00edk, R., Majumdar, R., (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20\u201322 Jan 2016, pp. 649\u2013662. ACM (2016)","DOI":"10.1145\/2837614.2837643"},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"Lamport, L.: How to make a multiprocessor that correctly executes multiprocess programs. IEEE Trans. Comput. C-28, 690\u2013691 (1979)","DOI":"10.1109\/TC.1979.1675439"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"Liu, S., Seemakhupt, K., Wei, Y., Wenisch, T.F., Kolli, A., Khan, S.: Cross failure bug detection in persistent memory programs. In: ASPLOS (2020)","DOI":"10.1145\/3373376.3378452"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Raad, A., Wickerson, J., Neiger, G., Vafeiadis, V.: Persistency semantics of the intel-x86 architecture. In: PACMPL, vol. 4, no. POPL, pp. 1\u201331 (2020)","DOI":"10.1145\/3371079"},{"key":"24_CR24","doi-asserted-by":"crossref","unstructured":"Ros, A., Kaxiras, S.: Racer: TSO consistency via race detection. In: MICRO (2016)","DOI":"10.1109\/MICRO.2016.7783736"},{"key":"24_CR25","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding Power Multiprocessors. In: PLDI 2011, 175\u2013186 (2011)","DOI":"10.1145\/1993316.1993520"},{"key":"24_CR26","doi-asserted-by":"crossref","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)","DOI":"10.1145\/1785414.1785443"}],"container-title":["Lecture Notes in Computer Science","Principles of Systems Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-22337-2_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,11]],"date-time":"2024-10-11T02:55:29Z","timestamp":1728615329000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-22337-2_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031223365","9783031223372"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-22337-2_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}