{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:08:38Z","timestamp":1776305318009,"version":"3.50.1"},"publisher-location":"Cham","reference-count":64,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030945824","type":"print"},{"value":"9783030945831","type":"electronic"}],"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.springer.com\/tdm"},{"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.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-030-94583-1_20","type":"book-chapter","created":{"date-parts":[[2022,1,13]],"date-time":"2022-01-13T22:02:34Z","timestamp":1642111354000},"page":"400-424","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Stateful Dynamic Partial Order Reduction for\u00a0Model Checking Event-Driven Applications that\u00a0Do Not Terminate"],"prefix":"10.1007","author":[{"given":"Rahmadi","family":"Trimananda","sequence":"first","affiliation":[]},{"given":"Weiyu","family":"Luo","sequence":"additional","affiliation":[]},{"given":"Brian","family":"Demsky","sequence":"additional","affiliation":[]},{"given":"Guoqing Harry","family":"Xu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,1,14]]},"reference":[{"key":"20_CR1","unstructured":"Lock it when i leave (2015). https:\/\/github.com\/SmartThingsCommunity\/SmartThingsPublic\/blob\/61b864535321a6f61cf5a77216f1e779bde68bd5\/smartapps\/smartthings\/lock-it-when-i-leave.src\/lock-it-when-i-leave.groovy"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: Proceedings of the 2014 Symposium on Principles of Programming Languages, pp. 373\u2013384 (2014). http:\/\/doi.acm.org\/10.1145\/2535838.2535845","DOI":"10.1145\/2578855.2535845"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. In: Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 353\u2013367 (2015). http:\/\/link.springer.com\/chapter\/10.1007","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"20_CR4","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., Ngo, T.P.: Optimal stateless model checking under the release-acquire semantics. Proc. ACM Program. Lang. 2(OOPSLA) (2018). https:\/\/doi.org\/10.1145\/3276505","DOI":"10.1145\/3276505"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Alur, R., Martin, M.M.K.: CheckFence: checking consistency of concurrent data types on relaxed memory models. In: Proceedings of the 2007 Conference on Programming Language Design and Implementation, pp. 12\u201321 (2007). http:\/\/doi.acm.org\/10.1145\/1250734.1250737","DOI":"10.1145\/1273442.1250737"},{"key":"20_CR6","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Pavlogiannis, A., Toman, V.: Value-centric dynamic partial order reduction. Proc. ACM Program. Lang. 3(OOPSLA) (2019). https:\/\/doi.org\/10.1145\/3360550","DOI":"10.1145\/3360550"},{"issue":"3","key":"20_CR7","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)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"20_CR8","unstructured":"Clarke Jr, E.M., Grumberg, O., Peled, D.: Model Checking. MIT press, Cambridge (1999)"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Demsky, B., Lam, P.: SATCheck: SAT-directed stateless model checking for SC and TSO. In: Proceedings of the 2015 Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 20\u201336 (October 2015). http:\/\/doi.acm.org\/10.1145\/2814270.2814297","DOI":"10.1145\/2814270.2814297"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Desai, A., Qadeer, S., Seshia, S.A.: Systematic testing of asynchronous reactive systems. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, pp. 73\u201383 (2015)","DOI":"10.1145\/2786805.2786861"},{"issue":"5","key":"20_CR11","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1145\/949952.940107","volume":"28","author":"MB Dwyer","year":"2003","unstructured":"Dwyer, M.B., Hatcliff, J.: Bogor: an extensible and highly-modular software model checking framework. ACM SIGSOFT Softw. Eng. Notes 28(5), 267\u2013276 (2003)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"issue":"1","key":"20_CR12","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1145\/1047659.1040315","volume":"40","author":"C Flanagan","year":"2005","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. ACM Sigplan Not. 40(1), 110\u2013121 (2005)","journal-title":"ACM Sigplan Not."},{"key":"20_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem","author":"P Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer-Verlag, Berlin, Heidelberg (1996)"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using verisoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 174\u2013186 (1997)","DOI":"10.1145\/263699.263717"},{"issue":"2","key":"20_CR15","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. Form. Methods Syst. Des. 26(2), 77\u2013101 (2005)","journal-title":"Form. Methods Syst. Des."},{"key":"20_CR16","unstructured":"Google: Android things website (2015). https:\/\/developer.android.com\/things\/"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-540-73370-6_8","volume-title":"Model Checking Software","author":"G Gueta","year":"2007","unstructured":"Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 95\u2013112. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73370-6_8"},{"key":"20_CR18","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual, vol. 1003 (2003)"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Huang, J.: Stateless model checking concurrent programs with maximal causality reduction. In: Proceedings of the 2015 Conference on Programming Language Design and Implementation, pp. 165\u2013174 (2015). http:\/\/doi.acm.org\/10.1145\/2813885.2737975","DOI":"10.1145\/2813885.2737975"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"Huang, S., Huang, J.: Maximal causality reduction for TSO and PSO. In: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 447\u2013461 (2016). http:\/\/doi.acm.org\/10.1145\/2983990.2984025","DOI":"10.1145\/2983990.2984025"},{"key":"20_CR21","unstructured":"IFTTT: IFTTT (September 2011). https:\/\/www.ifttt.com\/"},{"issue":"10","key":"20_CR22","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1145\/2858965.2814282","volume":"50","author":"CS Jensen","year":"2015","unstructured":"Jensen, C.S., M\u00f8ller, A., Raychev, V., Dimitrov, D., Vechev, M.: Stateless model checking of event-driven applications. ACM SIGPLAN Not. 50(10), 57\u201373 (2015)","journal-title":"ACM SIGPLAN Not."},{"issue":"2","key":"20_CR23","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/0304-3975(92)90054-J","volume":"101","author":"S Katz","year":"1992","unstructured":"Katz, S., Peled, D.: Defining conditional independence using collapses. Theor. Comput. Sci. 101(2), 337\u2013359 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"20_CR24","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for C\/C++ concurrency. Proc. ACM Program. Lang. 2(POPL) (2017). https:\/\/doi.org\/10.1145\/3158105","DOI":"10.1145\/3158105"},{"key":"20_CR25","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Raad, A., Vafeiadis, V.: Effective lock handling in stateless model checking. Proc. ACM Program. Lang. 3(OOPSLA) (2019). https:\/\/doi.org\/10.1145\/3360599","DOI":"10.1145\/3360599"},{"key":"20_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-642-12029-9_22","volume-title":"Fundamental Approaches to Software Engineering","author":"S Lauterburg","year":"2010","unstructured":"Lauterburg, S., Karmani, R.K., Marinov, D., Agha, G.: Evaluating ordering heuristics for dynamic partial-order reduction techniques. In: Rosenblum, D.S., Taentzer, G. (eds.) FASE 2010. LNCS, vol. 6013, pp. 308\u2013322. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12029-9_22"},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"Li, X., Zhang, L., Shen, X.: IA-graph based inter-app conflicts detection in open IoT systems. In: Proceedings of the 20th ACM SIGPLAN\/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems, pp. 135\u2013147 (2019)","DOI":"10.1145\/3316482.3326350"},{"key":"20_CR28","unstructured":"Li, X., Zhang, L., Shen, X., Qi, Y.: A systematic examination of inter-app conflicts detections in open IoT systems. Technical report TR-2017-1, North Carolina State University, Dept. of Computer Science (2017)"},{"key":"20_CR29","doi-asserted-by":"crossref","unstructured":"Loring, M.C., Marron, M., Leijen, D.: Semantics of asynchronous Javascript. In: Proceedings of the 13th ACM SIGPLAN International Symposium on on Dynamic Languages, pp. 51\u201362 (2017)","DOI":"10.1145\/3133841.3133846"},{"key":"20_CR30","doi-asserted-by":"crossref","unstructured":"Maiya, P., Gupta, R., Kanade, A., Majumdar, R.: Partial order reduction for event-driven multi-threaded programs. In: Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 16) (2016)","DOI":"10.1007\/978-3-662-49674-9_44"},{"key":"20_CR31","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). https:\/\/doi.org\/10.1007\/3-540-17906-2_30"},{"key":"20_CR32","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Park, D.Y., Chou, A., Engler, D.R., Dill, D.L.: CMC: a pragmatic approach to model checking real code. ACM SIGOPS Oper. Syst. Rev. 36(SI), 75\u201388 (2002)","DOI":"10.1145\/844128.844136"},{"key":"20_CR33","unstructured":"Musuvathi, M., Qadeer, S., Ball, T.: Chess: a systematic testing tool for concurrent software (2007)"},{"issue":"1","key":"20_CR34","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2557833.2560581","volume":"39","author":"E Noonan","year":"2014","unstructured":"Noonan, E., Mercer, E., Rungta, N.: Vector-clock based partial order reduction for JPF. SIGSOFT Softw. Eng. Notes 39(1), 1\u20135 (2014)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"20_CR35","unstructured":"openHAB: openhab website (2010). https:\/\/www.openhab.org\/"},{"key":"20_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/978-3-319-21690-4_28","volume-title":"Computer Aided Verification","author":"BK Ozkan","year":"2015","unstructured":"Ozkan, B.K., Emmi, M., Tasiran, S.: Systematic asynchrony bug exploration for android apps. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 455\u2013461. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_28"},{"key":"20_CR37","doi-asserted-by":"crossref","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: Proceedings of the International Conference on Computer Aided Verification, pp. 377\u2013390 (1994)","DOI":"10.1007\/3-540-58179-0_69"},{"key":"20_CR38","unstructured":"Racine, Y.: Fireco2alarm smartapp (2014). https:\/\/github.com\/yracine\/device-type.myecobee\/blob\/master\/smartapps\/FireCO2Alarm.src\/FireCO2Alarm.groovy"},{"key":"20_CR39","unstructured":"Racine, Y.: grovestreams smartapp (2014). https:\/\/github.com\/uci-plrg\/iotcheck\/blob\/master\/smartapps\/groveStreams.groovy"},{"key":"20_CR40","unstructured":"Rodr\u00edguez, C., Sousa, M., Sharma, S., Kroening, D.: Unfolding-based partial order reduction. In: CONCUR (2015)"},{"key":"20_CR41","doi-asserted-by":"crossref","unstructured":"Saarikivi, O., K\u00e4hk\u00f6nen, K., Heljanko, K.: Improving dynamic partial order reductions for concolic testing. In: 2012 12th International Conference on Application of Concurrency to System Design, pp. 132\u2013141. IEEE (2012)","DOI":"10.1109\/ACSD.2012.18"},{"key":"20_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/11693017_25","volume-title":"Fundamental Approaches to Software Engineering","author":"K Sen","year":"2006","unstructured":"Sen, K., Agha, G.: Automated systematic testing of open distributed programs. In: Baresi, L., Heckel, R. (eds.) FASE 2006. LNCS, vol. 3922, pp. 339\u2013356. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11693017_25"},{"key":"20_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-540-70889-6_13","volume-title":"Hardware and Software, Verification and Testing","author":"K Sen","year":"2007","unstructured":"Sen, K., Agha, G.: A race-detection and flipping algorithm for automated testing of multi-threaded programs. In: Bin, E., Ziv, A., Ur, S. (eds.) HVC 2006. LNCS, vol. 4383, pp. 166\u2013182. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-70889-6_13"},{"key":"20_CR44","unstructured":"SmartThings: Device handlers (2018). https:\/\/docs.smartthings.com\/en\/latest\/device-type-developers-guide\/"},{"key":"20_CR45","unstructured":"SmartThings: Smartthings public github repo (2018). https:\/\/github.com\/SmartThingsCommunity\/SmartThingsPublic"},{"key":"20_CR46","unstructured":"SmartThings, S.: Samsung smartthings website (2012). http:\/\/www.smartthings.com"},{"key":"20_CR47","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). https:\/\/doi.org\/10.1007\/978-3-642-30793-5_14"},{"key":"20_CR48","unstructured":"Trimananda, R., Aqajari, S.A.H., Chuang, J., Demsky, B., Xu, G.H., Lu, S.: Iotcheck supporting materials (2020). https:\/\/github.com\/uci-plrg\/iotcheck-data\/tree\/master\/Device"},{"key":"20_CR49","doi-asserted-by":"crossref","unstructured":"Trimananda, R., Aqajari, S.A.H., Chuang, J., Demsky, B., Xu, G.H., Lu, S.: Understanding and automatically detecting conflicting interactions between smart home IoT applications. In: Proceedings of the ACM SIGSOFT International Symposium on Foundations of Software Engineering (November 2020)","DOI":"10.1145\/3368089.3409682"},{"key":"20_CR50","doi-asserted-by":"publisher","unstructured":"Trimananda, R., Luo, W., Demsky, B., Xu, G.H.: Iotcheck dpor (2021). https:\/\/github.com\/uci-plrg\/iotcheck-dpor, https:\/\/doi.org\/10.5281\/zenodo.5168843, https:\/\/zenodo.org\/record\/5168843#.YQ8KjVNKh6c","DOI":"10.5281\/zenodo.5168843"},{"key":"20_CR51","doi-asserted-by":"crossref","unstructured":"Trimananda, R., Luo, W., Demsky, B., Xu, G.H.: Stateful dynamic partial order reduction for model checking event-driven applications that do not terminate. arXiv preprint arXiv:2111.05290 (2021)","DOI":"10.1007\/978-3-030-94583-1_20"},{"key":"20_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/BFb0023729","volume-title":"Computer-Aided Verification","author":"A Valmari","year":"1991","unstructured":"Valmari, A.: A stubborn attack on state explosion. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 156\u2013165. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0023729"},{"key":"20_CR53","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"},{"issue":"2","key":"20_CR54","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1109\/TII.2011.2166772","volume":"8","author":"PA Vicaire","year":"2012","unstructured":"Vicaire, P.A., Hoque, E., Xie, Z., Stankovic, J.A.: Bundle: a group-based programming abstraction for cyber-physical systems. IEEE Trans. Ind. Inf. 8(2), 379\u2013392 (2012)","journal-title":"IEEE Trans. Ind. Inf."},{"key":"20_CR55","doi-asserted-by":"crossref","unstructured":"Vicaire, P.A., Xie, Z., Hoque, E., Stankovic, J.A.: Physicalnet: a generic framework for managing and programming across pervasive computing networks. In: Real-Time and Embedded Technology and Applications Symposium (RTAS), 2010 16th IEEE, pp. 269\u2013278. IEEE (2010)","DOI":"10.1109\/RTAS.2010.17"},{"key":"20_CR56","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs 10, 203\u2013232 (2003)","DOI":"10.1023\/A:1022920129859"},{"key":"20_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-88387-6_11","volume-title":"Automated Technology for Verification and Analysis","author":"C Wang","year":"2008","unstructured":"Wang, C., Yang, Yu., Gupta, A., Gopalakrishnan, G.: Dynamic model checking with property driven pruning to detect race conditions. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 126\u2013140. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88387-6_11"},{"key":"20_CR58","doi-asserted-by":"crossref","unstructured":"Wood, A.D., et al.: Context-aware wireless sensor networks for assisted living and residential monitoring. IEEE Netw. 22(4) (2008)","DOI":"10.1109\/MNET.2008.4579768"},{"key":"20_CR59","doi-asserted-by":"crossref","unstructured":"Yagita, M., Ishikawa, F., Honiden, S.: An application conflict detection and resolution system for smart homes. In: Proceedings of the First International Workshop on Software Engineering for Smart Cyber-Physical Systems, pp. 33\u201339. SEsCPS 2015, IEEE Press, Piscataway, NJ, USA (2015). http:\/\/dl.acm.org\/citation.cfm?id=2821404.2821413","DOI":"10.1109\/SEsCPS.2015.14"},{"key":"20_CR60","doi-asserted-by":"crossref","unstructured":"Yang, Y., Chen, X., Gopalakrishnan, G., Kirby, R.M.: Distributed dynamic partial order reduction based verification of threaded software. In: Proceedings of the 14th International SPIN Conference on Model Checking Software, pp. 58\u201375 (2007)","DOI":"10.1007\/978-3-540-73370-6_6"},{"key":"20_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-540-85114-1_20","volume-title":"Model Checking Software","author":"Yu Yang","year":"2008","unstructured":"Yang, Yu., Chen, X., Gopalakrishnan, G., Kirby, R.M.: Efficient stateful dynamic partial order reduction. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 288\u2013305. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85114-1_20"},{"key":"20_CR62","doi-asserted-by":"crossref","unstructured":"Yang, Y., Chen, X., Gopalakrishnan, G., Wang, C.: Automatic discovery of transition symmetry in multithreaded programs using dynamic analysis. In: Proceedings of the 16th International SPIN Workshop on Model Checking Software, pp. 279\u2013295 (2009)","DOI":"10.1007\/978-3-642-02652-2_22"},{"key":"20_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/11901433_9","volume-title":"Formal Methods and Software Engineering","author":"X Yi","year":"2006","unstructured":"Yi, X., Wang, J., Yang, X.: Stateful dynamic partial-order reduction. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 149\u2013167. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11901433_9"},{"key":"20_CR64","doi-asserted-by":"crossref","unstructured":"Zhang, N., Kusano, M., Wang, C.: Dynamic partial order reduction for relaxed memory models. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 250\u2013259 (2015). http:\/\/doi.acm.org\/10.1145\/2737924.2737956","DOI":"10.1145\/2737924.2737956"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-94583-1_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,14]],"date-time":"2022-01-14T00:06:32Z","timestamp":1642118792000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-94583-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030945824","9783030945831"],"references-count":64,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-94583-1_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"14 January 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Philadelphia, PA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","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":"16 January 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 January 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl22.sigplan.org\/home\/VMCAI-2022","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":"63","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":"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":"37% - 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","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":"6","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)"}}]}}