{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T02:42:47Z","timestamp":1761964967885,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319899626"},{"type":"electronic","value":"9783319899633"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89963-3_14","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T14:53:00Z","timestamp":1523631180000},"page":"229-248","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":30,"title":["Optimal Dynamic Partial Order Reduction with Observers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1035-8378","authenticated-orcid":false,"given":"Stavros","family":"Aronis","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7897-601X","authenticated-orcid":false,"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0984-4229","authenticated-orcid":false,"given":"Magnus","family":"L\u00e5ng","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9657-0179","authenticated-orcid":false,"given":"Konstantinos","family":"Sagonas","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"key":"14_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). \n                      https:\/\/doi.org\/10.1007\/978-3-662-46681-0_28"},{"issue":"4","key":"14_CR2","doi-asserted-by":"publisher","first-page":"251","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), 251\u20132549 (2017). \n                      http:\/\/doi.acm.org\/10.1145\/3073408","journal-title":"J. ACM"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/978-3-319-63387-9_26","volume-title":"Computer Aided Verification","author":"E Albert","year":"2017","unstructured":"Albert, E., Arenas, P., de la Banda, M.G., G\u00f3mez-Zamalloa, M., Stuckey, P.J.: Context-sensitive dynamic partial order reduction. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 526\u2013543. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-63387-9_26"},{"issue":"9","key":"14_CR4","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/1810891.1810910","volume":"53","author":"J Armstrong","year":"2010","unstructured":"Armstrong, J.: Erlang. Commun. ACM 53(9), 68\u201375 (2010). \n                      http:\/\/doi.acm.org\/10.1145\/1810891.1810910","journal-title":"Commun. ACM"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-319-66845-1_15","volume-title":"Integrated Formal Methods","author":"S Aronis","year":"2017","unstructured":"Aronis, S., Fritchie, S.L., Sagonas, K.: Testing and verifying chain repair methods for Corfu using stateless model checking. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 227\u2013242. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-66845-1_15"},{"key":"14_CR6","doi-asserted-by":"publisher","unstructured":"Aronis, S., Jonsson, B., L\u00e5ng, M., Sagonas, K.: Binary artifact for TACAS-2018 paper \u201cOptimal DPOR with Observers\u201d. Figshare, February 2018. \n                      https:\/\/doi.org\/10.6084\/m9.figshare.5918701.v1","DOI":"10.6084\/m9.figshare.5918701.v1"},{"issue":"POPL","key":"14_CR7","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). \n                      http:\/\/doi.acm.org\/10.1145\/3158119","journal-title":"Proc. ACM Program. Lang."},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Christakis, M., Gotovos, A., Sagonas, K.: Systematic testing for detecting concurrency errors in Erlang programs. In: Sixth IEEE International Conference on Software Testing, Verification and Validation, ICST 2013, pp. 154\u2013163. IEEE Computer Society, Los Alamitos, CA, USA (2013). \n                      https:\/\/doi.org\/10.1109\/ICST.2013.50","DOI":"10.1109\/ICST.2013.50"},{"issue":"3","key":"14_CR9","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.: State space reduction using partial order techniques. Int. J. Softw. Tools Technol. Transf. 2(3), 279\u2013287 (1999). \n                      http:\/\/dx.doi.org\/10.1007\/s100090050035","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"14_CR10","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, pp. 110\u2013121. ACM, New York (2005). \n                      http:\/\/doi.acm.org\/10.1145\/1040305.1040315"},{"key":"14_CR11","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). \n                      http:\/\/www.springer.com\/gp\/book\/9783540607618\n                      \n                    , also. LNCS, vol. 1032. Springer, Heidelberg"},{"key":"14_CR12","unstructured":"Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1997, pp. 174\u2013186. ACM, New York (1997). \n                      http:\/\/doi.acm.org\/10.1145\/263699.263717"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/3-540-56922-7_36","volume-title":"Computer Aided Verification","author":"P Godefroid","year":"1993","unstructured":"Godefroid, P., Pirottin, D.: Refining dependencies improves partial-order verification methods (extended abstract). In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 438\u2013449. Springer, Heidelberg (1993). \n                      https:\/\/doi.org\/10.1007\/3-540-56922-7_36"},{"key":"14_CR14","unstructured":"Hartmanns, A., Wendler, P.: TACAS 2018 Artifact Evaluation VM. Figshare (2018). \n                      https:\/\/doi.org\/10.6084\/m9.figshare.5896615"},{"issue":"7","key":"14_CR15","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978). \n                      http:\/\/doi.acm.org\/10.1145\/359545.359563","journal-title":"Commun. ACM"},{"issue":"1","key":"14_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/7351.7352","volume":"5","author":"L Lamport","year":"1987","unstructured":"Lamport, L.: A fast mutual exclusion algorithm. ACM Trans. Comput. Syst. 5(1), 1\u201311 (1987). \n                      http:\/\/doi.acm.org\/10.1145\/7351.7352","journal-title":"ACM Trans. Comput. Syst."},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"680","DOI":"10.1007\/978-3-662-49674-9_44","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Maiya","year":"2016","unstructured":"Maiya, P., Gupta, R., Kanade, A., Majumdar, R.: Partial order reduction for event-driven multi-threaded programs. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 680\u2013697. Springer, Heidelberg (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-662-49674-9_44"},{"key":"14_CR18","unstructured":"Mattern, F.: Virtual time and global states of distributed systems. In: Cosnard, M., et al. (eds.) Proceedings of the Workshop on Parallel and Distributed Algorithms, pp. 215\u2013226. North-Holland\/Elsevier (1989)"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/3-540-17906-2_30","volume-title":"Petri Nets: Applications and Relationships to Other Models of Concurrency","author":"A Mazurkiewicz","year":"1987","unstructured":"Mazurkiewicz, A.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 255, pp. 278\u2013324. Springer, Heidelberg (1987). \n                      https:\/\/doi.org\/10.1007\/3-540-17906-2_30"},{"key":"14_CR20","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). \n                      https:\/\/doi.org\/10.1007\/3-540-56922-7_34"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-642-30793-5_14","volume-title":"Formal Techniques for Distributed Systems","author":"S Tasharofi","year":"2012","unstructured":"Tasharofi, S., Karmani, R.K., Lauterburg, S., Legay, A., Marinov, D., Agha, G.: TransDPOR: a novel dynamic partial-order reduction technique for testing actor programs. In: Giese, H., Rosu, G. (eds.) FMOODS\/FORTE -2012. LNCS, vol. 7273, pp. 219\u2013234. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-30793-5_14"},{"key":"14_CR22","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). \n                      https:\/\/doi.org\/10.1007\/3-540-53863-1_36"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89963-3_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,3]],"date-time":"2020-03-03T03:16:41Z","timestamp":1583205401000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89963-3_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319899626","9783319899633"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89963-3_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"14 April 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Thessaloniki","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 April 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 April 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/index.php\/2018\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}