{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T08:41:26Z","timestamp":1726044086924},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030312763"},{"type":"electronic","value":"9783030312770"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-31277-0_1","type":"book-chapter","created":{"date-parts":[[2019,9,13]],"date-time":"2019-09-13T12:02:53Z","timestamp":1568376173000},"page":"3-18","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial)"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[]},{"given":"Tuan Phong","family":"Ngo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,9,14]]},"reference":[{"key":"1_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). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_28"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: Symposium on Principles of Programming Languages, (POPL), pp. 373\u2013384. ACM, San Diego (2014)","DOI":"10.1145\/2535838.2535845"},{"issue":"4","key":"1_CR3","doi-asserted-by":"publisher","first-page":"25:1","DOI":"10.1145\/3073408","volume":"64","author":"PA Abdulla","year":"2017","unstructured":"Abdulla, P.A., Aronis, S., Jonsson, B., Sagonas, K.: Source sets: a foundation for optimal dynamic partial order reduction. J. ACM 64(4), 25:1\u201325:49 (2017). https:\/\/doi.org\/10.1145\/3073408","journal-title":"J. ACM"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-319-41540-6_8","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2016","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., Leonardsson, C.: Stateless model checking for POWER. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 134\u2013156. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_8"},{"issue":"OOPSLA","key":"1_CR5","doi-asserted-by":"publisher","first-page":"135:1","DOI":"10.1145\/3276505","volume":"2","author":"PA Abdulla","year":"2018","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., Ngo, T.P.: Optimal stateless model checking under the release-acquire semantics. PACMPL 2(OOPSLA), 135:1\u2013135:29 (2018). https:\/\/doi.org\/10.1145\/3276505","journal-title":"PACMPL"},{"issue":"2","key":"1_CR6","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/j.ic.2005.05.008","volume":"202","author":"PA Abdulla","year":"2005","unstructured":"Abdulla, P.A., Bertrand, N., Rabinovich, A.M., Schnoebelen, P.: Verification of probabilistic systems with faulty communication. Inf. Comput. 202(2), 141\u2013165 (2005). https:\/\/doi.org\/10.1016\/j.ic.2005.05.008","journal-title":"Inf. Comput."},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-540-70545-1_33","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2008","unstructured":"Abdulla, P.A., Bouajjani, A., Cederberg, J., Haziza, F., Rezine, A.: Monotonic abstraction for programs with dynamic memory heaps. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 341\u2013354. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_33"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45220-1_1","volume-title":"Computer Science Logic","author":"PA Abdulla","year":"2003","unstructured":"Abdulla, P.A., Bouajjani, A., d\u2019Orso, J.: Deciding monotonic games. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 1\u201314. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45220-1_1"},{"key":"1_CR9","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). https:\/\/doi.org\/10.1109\/LICS.2004.1319629","DOI":"10.1109\/LICS.2004.1319629"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-642-36742-7_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2013","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L., Jonsson, B., Rezine, A.: An integrated specification and verification technique for highly concurrent data structures. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 324\u2013338. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_23"},{"key":"1_CR11","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":"1_CR12","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Kindahl, M., Peled, D.A.: An improved search strategy for lossy channel systems. In: Togashi, A., Mizuno, T., Shiratori, N., Higashino, T. (eds.) Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE X \/ PSTV XVII\u201997, IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE X) and Protocol Specification, Testing and Verification (PSTV XVII), 18\u201321 November 1997, Osaka, Japan, IFIP Conference Proceedings, vol. 107, pp. 251\u2013264. Chapman & Hall (1997)","DOI":"10.1007\/978-0-387-35271-8_16"},{"issue":"POPL","key":"1_CR13","doi-asserted-by":"publisher","first-page":"31:1","DOI":"10.1145\/3158119","volume":"2","author":"M Chalupa","year":"2017","unstructured":"Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., Vaidya, K.: Data-centric dynamic partial order reduction. Proc. ACM Program. Lang. 2(POPL), 31:1\u201331:30 (2017). https:\/\/doi.org\/10.1145\/3158119","journal-title":"Proc. ACM Program. Lang."},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Christakis, M., Gotovos, A., Sagonas, K.: Systematic testing for detecting concurrency errors in Erlang programs. In: International Conference on Software Testing. Verification and Validation, (ICST), pp. 154\u2013163. IEEE, Luxembourg (2013)","DOI":"10.1109\/ICST.2013.50"},{"issue":"3","key":"1_CR15","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s100090050035","volume":"2","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Minea, M., Peled, D.A.: State space reduction using partial order techniques. STTT 2(3), 279\u2013287 (1999)","journal-title":"STTT"},{"key":"1_CR16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of Model Checking","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8"},{"key":"1_CR17","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. The MIT Press, Cambridge (2009)"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Demsky, B., Lam, P.: Satcheck: Sat-directed stateless model checking for SC and TSO. In: Object-Oriented Programming, Systems, Languages, and Applications, (OOPSLA), pp. 20\u201336. ACM, Pittsburgh (2015)","DOI":"10.1145\/2858965.2814297"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Principles of Programming Languages, POPL, pp. 110\u2013121. ACM, Long Beach (2005)","DOI":"10.1145\/1047659.1040315"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Ph.D. thesis, University of Li\u00e9ge (1996). Also, volume 1032 of LNCS, Springer","DOI":"10.1007\/3-540-60761-7"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using VeriSoft. In: Principles of Programming Languages, POPL, pp. 174\u2013186. ACM Press, Paris (1997)","DOI":"10.1145\/263699.263717"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Hammer, B., Jagadeesan, L.: Model checking without a model: an analysis of the heart-beat monitor of a telephone switch using VeriSoft. In: Proceedings of ACM SIGSOFT International Symposium on Software Testing and Analysis. pp. 124\u2013133 (1998)","DOI":"10.1145\/271775.271800"},{"issue":"2","key":"1_CR23","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10703-005-1489-x","volume":"26","author":"P Godefroid","year":"2005","unstructured":"Godefroid, P.: Software model checking: the VeriSoft approach. Formal Methods Syst. Des. 26(2), 77\u2013101 (2005)","journal-title":"Formal Methods Syst. Des."},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Huang, J.: Stateless model checking concurrent programs with maximal causality reduction. In: Programming Language Design and Implementation, PLDI, pp. 165\u2013174. ACM, Portland (2015)","DOI":"10.1145\/2813885.2737975"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Huang, S., Huang, J.: Maximal causality reduction for TSO and PSO. In: Object-Oriented Programming, Systems, Languages, and Applications, (OOPSLA), pp. 447\u2013461. ACM, Amsterdam (2016)","DOI":"10.1145\/3022671.2984025"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for C\/C++ concurrency. In: POPL (2018, to appear). http:\/\/plv.mpi-sws.org\/rcmc\/","DOI":"10.1145\/3158105"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Kokologiannakis, M., Sagonas, K.: Stateless model checking of the linux kernel\u2019s hierarchical read-copy-update (tree RCU). In: Symposium on Model Checking of Software, SPIN, pp. 172\u2013181. ACM, Santa Barbara (2017)","DOI":"10.1145\/3092282.3092287"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Lahav, O., Giannarakis, N., Vafeiadis, V.: Taming release-acquire consistency. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20\u201322 January 2016, pp. 649\u2013662. ACM (2016)","DOI":"10.1145\/2837614.2837643"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Mazurkiewicz, A.: Trace theory. In: Advances in Petri Nets (1986)","DOI":"10.1007\/3-540-17906-2_30"},{"key":"1_CR30","unstructured":"Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: OSDI, pp. 267\u2013280. USENIX Association (2008)"},{"issue":"3","key":"1_CR31","doi-asserted-by":"publisher","first-page":"10:1","DOI":"10.1145\/2806886","volume":"38","author":"B Norris","year":"2016","unstructured":"Norris, B., Demsky, B.: A practical approach for model checking C\/C++11 code. ACM Trans. Program. Lang. Syst. 38(3), 10:1\u201310:51 (2016)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Computer Aided Verification","author":"D Peled","year":"1993","unstructured":"Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409\u2013423. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56922-7_34"},{"key":"1_CR33","unstructured":"Rodr\u00edguez, C., Sousa, M., Sharma, S., Kroening, D.: Unfolding-based partial order reduction. In: CONCUR 2015, pp. 456\u2013469 (2015)"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"Saarikivi, O., K\u00e4hk\u00f6nen, K., Heljanko, K.: Improving dynamic partial order reductions for concolic testing. In: Application of Concurrency to System Design, ACSD, pp. 132\u2013141. IEEE, Hamburg (2012)","DOI":"10.1109\/ACSD.2012.18"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Sen, K., Agha, G.: A race-detection and flipping algorithm for automated testing of multi-threaded programs. In: Haifa Verification Conference. pp. 166\u2013182 (2007), lNCS 4383","DOI":"10.1007\/978-3-540-70889-6_13"},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/3-540-53863-1_36","volume-title":"Advances in Petri Nets 1990","author":"A Valmari","year":"1991","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) ICATPN 1989. LNCS, vol. 483, pp. 491\u2013515. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-53863-1_36"},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Zhang, N., Kusano, M., Wang, C.: Dynamic partial order reduction for relaxed memory models. In: Programming Language Design and Implementation (PLDI), pp. 250\u2013259. ACM, Portland (2015)","DOI":"10.1145\/2813885.2737956"}],"container-title":["Lecture Notes in Computer Science","Networked Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-31277-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,28]],"date-time":"2022-09-28T17:11:07Z","timestamp":1664385067000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-31277-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030312763","9783030312770"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-31277-0_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"14 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NETYS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Networked Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Marrakech","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Morocco","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 June 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 June 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"netys2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/netys.net\/","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":"60","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":"23","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":"4","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":"38% - 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":"2.91","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":"3.68","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}