{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:19:56Z","timestamp":1781075996662,"version":"3.54.1"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2020,6,27]],"date-time":"2020-06-27T00:00:00Z","timestamp":1593216000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,6,27]],"date-time":"2020-06-27T00:00:00Z","timestamp":1593216000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"crossref","award":["PARDI (ANR-16-CE25-0006)"],"award-info":[{"award-number":["PARDI (ANR-16-CE25-0006)"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,10]]},"DOI":"10.1007\/s10817-020-09565-w","type":"journal-article","created":{"date-parts":[[2020,6,27]],"date-time":"2020-06-27T10:03:11Z","timestamp":1593252191000},"page":"1307-1330","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Parameterized Model Checking on the TSO Weak Memory Model"],"prefix":"10.1007","volume":"64","author":[{"given":"Sylvain","family":"Conchon","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0864-0953","authenticated-orcid":false,"given":"David","family":"Declerck","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fatiha","family":"Za\u00efdi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,6,27]]},"reference":[{"key":"9565_CR1","unstructured":"Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: The benefits of duality in verifying concurrent programs under TSO. In: 27th International Conference on Concurrency Theory, CONCUR 2016, August 23\u201326, 2016, Qu\u00e9bec City, Canada, pp. 5:1\u20135:15 (2016)"},{"key":"9565_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y., Leonardsson, C., Rezine, A.: Memorax, a precise and sound tool for automatic fence insertion under TSO. In: 19th International Conference Tools and Algorithms for the Construction and Analysis of Systems\u2014TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16\u201324, 2013. Proceedings, pp. 530\u2013536 (2013)","DOI":"10.1007\/978-3-642-36742-7_37"},{"key":"9565_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Delzanno, G., Henda, N.B., Rezine, A.: Regular model checking without transducers (on efficient verification of parameterized systems). In: 13th International Conference Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24\u2013April 1, 2007, Proceedings, pp. 721\u2013736 (2007)","DOI":"10.1007\/978-3-540-71209-1_56"},{"key":"9565_CR4","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, A.: Parameterized verification of infinite-state processes with global conditions. In: 19th International Conference on Computer Aided Verification, CAV 2007, Berlin, Germany, July 3\u20137, 2007, Proceedings, pp. 145\u2013157 (2007)","DOI":"10.1007\/978-3-540-73368-3_17"},{"key":"9565_CR5","unstructured":"Alglave, J.: A Shared Memory Poetics. Ph.D. thesis, University of Paris 7 - Denis Diderot, Paris, France (2010)"},{"key":"9565_CR6","unstructured":"Alglave, J., Fox, A.C.J., Ishtiaq, S., Myreen, M.O., Sarkar, S., Sewell, P., Nardelli, F.Z.: The semantics of power and ARM multiprocessor machine code. In: Proceedings of the POPL 2009 Workshop on Declarative Aspects of Multicore Programming, DAMP 2009, Savannah, GA, USA, January 20, 2009, pp. 13\u201324 (2009)"},{"key":"9565_CR7","doi-asserted-by":"crossref","unstructured":"Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: Programming Languages and Systems\u201422nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, pp. 512\u2013532 (2013)","DOI":"10.1007\/978-3-642-37036-6_28"},{"key":"9565_CR8","doi-asserted-by":"crossref","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: 25th International Conference on Computer Aided Verification\u2014CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013. Proceedings, pp. 141\u2013157 (2013)","DOI":"10.1007\/978-3-642-39799-8_9"},{"issue":"2","key":"9565_CR9","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."},{"issue":"6","key":"9565_CR10","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"KR Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"9565_CR11","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Calin, G., Derevenetc, E., Meyer, R.: Lazy TSO reachability. In: Fundamental Approaches to Software Engineering\u201418th International Conference, FASE 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11\u201318, 2015. Proceedings, pp. 267\u2013282 (2015)","DOI":"10.1007\/978-3-662-46675-9_18"},{"key":"9565_CR12","unstructured":"Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Programming Languages and Systems\u201422nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16\u201324, 2013. Proceedings, pp. 533\u2013553 (2013)"},{"key":"9565_CR13","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about networks with many identical finite-state processes. In: Proceedings of the Fifth Annual ACM Symposium on Principles of Distributed Computing, Calgary, Alberta, Canada, August 11\u201313, 1986, pp. 240\u2013248 (1986)","DOI":"10.1145\/10590.10611"},{"key":"9565_CR14","unstructured":"Conchon, S., Declerck, D., Za\u00efdi, F.: Cubicle-$$\\cal{W}$$: parameterized model checking on weak memory. In: 9th International Joint Conference System Descriptions\u2014IJCAR 2018, Oxford, United Kingdom, July 14\u201317, 2018, Proceedings (2018)"},{"key":"9565_CR15","doi-asserted-by":"crossref","unstructured":"Conchon, S., Goel, A., Krstic, S., Mebsout, A., Za\u00efdi, F.: Invariants for finite instances and beyond. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20\u201323, 2013, pp. 61\u201368 (2013)","DOI":"10.1109\/FMCAD.2013.6679392"},{"key":"9565_CR16","doi-asserted-by":"crossref","unstructured":"Conchon, S., Goel, A., Krstic, S., Mebsout, A., Za\u00efdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems\u2014tool paper. In: 24th International Conference on Computer Aided Verification, CAV 2012, Berkeley, CA, USA, July 7\u201313, 2012 Proceedings, pp. 718\u2013724 (2012)","DOI":"10.1007\/978-3-642-31424-7_55"},{"key":"9565_CR17","doi-asserted-by":"crossref","unstructured":"Conchon, S., Mebsout, A., Za\u00efdi, F.: Certificates for parameterized model checking. In: FM 2015: Formal Methods in 20th International Symposium, Oslo, Norway, June 24\u201326, 2015, Proceedings, pp. 126\u2013142 (2015)","DOI":"10.1007\/978-3-319-19249-9_9"},{"key":"9565_CR18","unstructured":"Cubicle-$$\\cal W\\it $$. http:\/\/cubicle.lri.fr\/cubiclew\/"},{"issue":"3","key":"9565_CR19","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"SM German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675\u2013735 (1992)","journal-title":"J. ACM"},{"key":"9565_CR20","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. LMCS 6(4) (2010)","DOI":"10.2168\/LMCS-6(4:10)2010"},{"key":"9565_CR21","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: 5th International Joint Conference Automated Reasoning, IJCAR 2010, Edinburgh, UK, July 16\u201319, 2010. Proceedings, pp. 22\u201329 (2010)","DOI":"10.1007\/978-3-642-14203-1_3"},{"key":"9565_CR22","doi-asserted-by":"crossref","first-page":"517","DOI":"10.3233\/FI-1981-4304","volume":"4","author":"HJM Goeman","year":"1981","unstructured":"Goeman, H.J.M.: The arbiter: an active system component for implementing synchronizing primitives. Fundam. Inform. 4, 517\u2013530 (1981)","journal-title":"Fundam. Inform."},{"key":"9565_CR23","volume-title":"The Art of Multiprocessor Programming","author":"M Herlihy","year":"2008","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann, Burlington (2008)"},{"issue":"9","key":"9565_CR24","doi-asserted-by":"publisher","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":"9565_CR25","doi-asserted-by":"crossref","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: 22nd International Conference Theorem Proving in Higher Order Logics, TPHOLs 2009, Munich, Germany, August 17\u201320, 2009. Proceedings, pp. 391\u2013407 (2009)","DOI":"10.1007\/978-3-642-03359-9_27"},{"issue":"7","key":"9565_CR26","doi-asserted-by":"publisher","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"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09565-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09565-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09565-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,6,26]],"date-time":"2021-06-26T23:09:12Z","timestamp":1624748952000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-020-09565-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,27]]},"references-count":26,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2020,10]]}},"alternative-id":["9565"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09565-w","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,6,27]]},"assertion":[{"value":"5 May 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 May 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 June 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}