{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T10:48:31Z","timestamp":1747133311410,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031258022"},{"type":"electronic","value":"9783031258039"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[[2023]]},"DOI":"10.1007\/978-3-031-25803-9_6","type":"book-chapter","created":{"date-parts":[[2023,1,31]],"date-time":"2023-01-31T20:10:16Z","timestamp":1675195816000},"page":"92-110","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["SMT-Based Verification of\u00a0Persistency Invariants of\u00a0Px86 Programs"],"prefix":"10.1007","author":[{"given":"Iason","family":"Marmanis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,2,1]]},"reference":[{"key":"6_CR1","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 concurrent software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 141\u2013157. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_9"},{"key":"6_CR2","doi-asserted-by":"publisher","unstructured":"Bender, M.A., Fineman, J.T., Gilbert, S., Tarjan, R.E.: A new approach to incremental cycle detection and related problems. ACM Trans. Algorithms 12(2) (2015). https:\/\/doi.org\/10.1145\/2756553. ISSN 1549-6325","DOI":"10.1145\/2756553"},{"key":"6_CR3","doi-asserted-by":"publisher","unstructured":"Cho, K., Lee, S.-H., Raad, A., Kang, J.: Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-X86 and Armv8. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021. Virtual, Canada, pp. 16\u201331. Association for Computing Machinery (2021). https:\/\/doi.org\/10.1145\/3453483.3454027. ISBN 9781450383912","DOI":"10.1145\/3453483.3454027"},{"key":"6_CR4","doi-asserted-by":"publisher","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Kenneth Zadeck, F.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451\u2013490 (1991). https:\/\/doi.org\/10.1145\/115372.115320. ISSN 0164-0925","DOI":"10.1145\/115372.115320"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962). https:\/\/doi.org\/10.1145\/368273.368557. ISSN 0001-0782","DOI":"10.1145\/368273.368557"},{"key":"6_CR6","doi-asserted-by":"publisher","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960). https:\/\/doi.org\/10.1145\/321033.321034. ISSN 0004-5411","DOI":"10.1145\/321033.321034"},{"key":"6_CR7","doi-asserted-by":"publisher","unstructured":"Friedman, M., Herlihy, M., Marathe, V., Petrank, E.: A persistent lock-free queue for non-volatile memory. In: Proceedings of the 23rd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2018, Vienna, Austria, pp. 28\u201340. Association for Computing Machinery (2018). https:\/\/doi.org\/10.1145\/3178487.3178490. ISBN 9781450349826","DOI":"10.1145\/3178487.3178490"},{"key":"6_CR8","doi-asserted-by":"publisher","unstructured":"Frigioni, D., Miller, T., Nanni, U., Zaroliagis, C.: An experimental study of dynamic algorithms for transitive closure. ACM J. Exp. Algorithmics 6, 9-es (2002). https:\/\/doi.org\/10.1145\/945394.945403. ISSN 1084-6654","DOI":"10.1145\/945394.945403"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175\u2013188. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_14 ISBN 978-3-540-27813-9"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"Gorjiara, H., Xu, G.H., Demsky, B.: Jaaru: efficiently model checking persistent memory programs. In: Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 415\u2013428. Association for Computing Machinery, New York (2021). https:\/\/doi.org\/10.1145\/3445814.3446735. ISBN 9781450383172","DOI":"10.1145\/3445814.3446735"},{"key":"6_CR11","doi-asserted-by":"publisher","unstructured":"He, F., Sun, Z., Fan, H.: Satisfiability modulo ordering consistency theory for multi-threaded program verification. In: Proceedings of the 42nd CM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021. Virtual, Canada, pp. 1264\u20131279. Association for Computing Machinery (2021). https:\/\/doi.org\/10.1145\/3453483.3454108. ISBN 9781450383912","DOI":"10.1145\/3453483.3454108"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Italiano, G.F.: Amortized efficiency of a path retrieval data structure. Theor. Comput. Sci. 48(2-3), 273\u2013281 (1987). ISSN 0304-3975","DOI":"10.1016\/0304-3975(86)90098-8"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-662-53426-7_23","volume-title":"Distributed Computing","author":"J Izraelevitz","year":"2016","unstructured":"Izraelevitz, J., Mendes, H., Scott, M.L.: Linearizability of persistent memory objects under a full-system-crash failure model. In: Gavoille, C., Ilcinkas, D. (eds.) DISC 2016. LNCS, vol. 9888, pp. 313\u2013327. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53426-7_23 ISBN 978-3-662-53425-0"},{"key":"6_CR14","doi-asserted-by":"publisher","unstructured":"Khyzha, A., Lahav, O.: Taming X86-TSO persistency. Proc. ACM Program. Lang. 5(POPL) (2021). https:\/\/doi.org\/10.1145\/3434328","DOI":"10.1145\/3434328"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Kaysin, I., Raad, A., Vafeiadis, V.: PerSeVerE: persistency semantics for verification under ext4. Proc. ACM Program. Lang. 5(POPL) (2021). https:\/\/doi.org\/10.1145\/3434324","DOI":"10.1145\/3434324"},{"key":"6_CR16","doi-asserted-by":"publisher","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers 28(9), 690\u2013691 (1979). https:\/\/doi.org\/10.1109\/TC.1979.1675439","DOI":"10.1109\/TC.1979.1675439"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Lantz, P., Dulloor, S., Kumar, S., Sankaran, R., Jackson, J.: Yat: a validation framework for persistent memory software. In: Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference, USENIX ATC 2014, pp. 433\u2013438. USENIX Association, Philadelphia (2014). ISBN 9781931971102","DOI":"10.1145\/2592798.2592814"},{"key":"6_CR18","doi-asserted-by":"publisher","unstructured":"Liu, S., Wei, Y., Zhao, J., Kolli, A., Khan, S.M.: PMTest: a fast and flexible testing framework for persistent memory programs. In: Bahar, I., Herlihy, M., Witchel, E., Lebeck, A.R. (eds.) ASPLOS 2019, pp. 411\u2013425. ACM (2019). https:\/\/doi.org\/10.1145\/3297858.3304015","DOI":"10.1145\/3297858.3304015"},{"key":"6_CR19","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 de Moura","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 ISBN 978-3-540-78800-3"},{"key":"6_CR20","doi-asserted-by":"publisher","unstructured":"Oukid, I., Booss, D., Lespinasse, A., Lehner, W.: On testing persistent-memory-based software. In: DaMoN 2016. ACM (2016). https:\/\/doi.org\/10.1145\/2933349.2933354. ISBN 9781450343190","DOI":"10.1145\/2933349.2933354"},{"key":"6_CR21","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). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_27 ISBN 978-3-642-03358-2"},{"key":"6_CR22","doi-asserted-by":"publisher","unstructured":"Raad, A., Maranget, L., Vafeiadis, V.: Extending Intel-X86 consistency and persistency: formalising the semantics of Intel-X86 memory types and non-temporal stores. Proc. ACM Program. Lang. 6(POPL) (2022). https:\/\/doi.org\/10.1145\/3498683","DOI":"10.1145\/3498683"},{"key":"6_CR23","doi-asserted-by":"publisher","unstructured":"Raad, A., Vafeiadis, V.: Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model. Proc. ACM Program. Lang. 2(OOPSLA) (2018). https:\/\/doi.org\/10.1145\/3276507","DOI":"10.1145\/3276507"},{"key":"6_CR24","doi-asserted-by":"publisher","unstructured":"Raad, A., Wickerson, J., Neiger, G., Vafeiadis, V.: Persistency semantics of the Intel-x86 architecture. Proc. ACM Program. Lang. 4(POPL), 11:1\u201311:31 (2019). https:\/\/doi.org\/10.1145\/3371079. Accessed 17 June 2020","DOI":"10.1145\/3371079"},{"key":"6_CR25","doi-asserted-by":"publisher","unstructured":"Raad, A., Wickerson, J., Vafeiadis, V.: Weak persistency semantics from the ground up. Proc. ACM Program. Lang. 3(OOPSLA), 135:1\u2013135:27 (2019). https:\/\/doi.org\/10.1145\/3360561. Accessed 07 Feb 2020","DOI":"10.1145\/3360561"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Wei, Y., Ben-David, N., Friedman, M., Blelloch, G.E., Petrank, E.: FliT: a library for simple and efficient persistent algorithms. CoRR abs\/2108.04202 (2021). arXiv:2108.04202","DOI":"10.1145\/3503221.3508436"},{"key":"6_CR27","doi-asserted-by":"publisher","unstructured":"Yin, L., Dong, W., Liu, W., Wang, J.: Scheduling constraint based abstraction refinement for multi-threaded program verification. IEEE Trans. Softw. Eng. (2017). https:\/\/doi.org\/10.1109\/TSE.2018.2864122","DOI":"10.1109\/TSE.2018.2864122"},{"key":"6_CR28","doi-asserted-by":"publisher","unstructured":"Yin, L., Dong, W., Liu, W., Wang, J.: Scheduling constraint based abstraction refinement for weak memory models. In: Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, pp. 645\u2013655. Association for Computing Machinery, New York (2018). https:\/\/doi.org\/10.1145\/3238147.3238223. ISBN 9781450359375","DOI":"10.1145\/3238147.3238223"},{"key":"6_CR29","doi-asserted-by":"publisher","unstructured":"Zuriel, Y., Friedman, M., Sheffi, G., Cohen, N., Petrank, E.: Efficient lock-free durable sets. Proc. ACM Program. Lang. 3(OOPSLA) (2019). https:\/\/doi.org\/10.1145\/3360554","DOI":"10.1145\/3360554"}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools and Experiments."],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-25803-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,31]],"date-time":"2023-01-31T20:21:17Z","timestamp":1675196477000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-25803-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031258022","9783031258039"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-25803-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"1 February 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Working Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Trento","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/vstte22.fbk.eu\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"45% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.1","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}