{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T18:17:00Z","timestamp":1773512220958,"version":"3.50.1"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030509941","type":"print"},{"value":"9783030509958","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-50995-8_7","type":"book-chapter","created":{"date-parts":[[2020,6,19]],"date-time":"2020-06-19T23:05:25Z","timestamp":1592607925000},"page":"122-140","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Testing for Race Conditions in\u00a0Distributed Systems via SMT Solving"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4671-4132","authenticated-orcid":false,"given":"Jo\u00e3o Carlos","family":"Pereira","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1531-1875","authenticated-orcid":false,"given":"Nuno","family":"Machado","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0892-3577","authenticated-orcid":false,"given":"Jorge","family":"Sousa Pinto","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,6,20]]},"reference":[{"key":"7_CR1","unstructured":"Apache Hadoop. \nhttp:\/\/hadoop.apache.org"},{"key":"7_CR2","unstructured":"Apache HBase. \nhttp:\/\/hbase.apache.org"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: STOC 1971. ACM (1971)","DOI":"10.1145\/800157.805047"},{"key":"7_CR4","unstructured":"The Coq proof assistant. \nhttps:\/\/coq.inria.fr\/"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-16576-4_13","volume-title":"Autonomic and Trusted Computing","author":"M Elwakil","year":"2010","unstructured":"Elwakil, M., Yang, Z., Wang, L., Chen, Q.: Message race detection for web services by an SMT-based analysis. In: Xie, B., Branke, J., Sadjadi, S.M., Zhang, D., Zhou, X. (eds.) ATC 2010. LNCS, vol. 6407, pp. 182\u2013194. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-16576-4_13"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Feng, Y., Martins, R., Bastani, O., Dillig, I.: Program synthesis using conflict-driven learning. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018. ACM (2018)","DOI":"10.1145\/3192366.3192382"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N.: FastTrack: efficient and precise dynamic race detection. In: PLDI 2009 (2009)","DOI":"10.1145\/1542476.1542490"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Guo, H., Wu, M., Zhou, L., Hu, G., Yang, J., Zhang, L.: Practical software model checking via dynamic interface reduction. In: SOSP 2011 (2011)","DOI":"10.1145\/2043556.2043582"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., et al.: IronFleet: proving practical distributed systems correct. In: SOSP 2015. ACM (2015)","DOI":"10.1145\/2815400.2815428"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Huang, J.: Stateless model checking concurrent programs with maximal causality reduction. In: PLDI 2015. ACM (2015)","DOI":"10.1145\/2737924.2737975"},{"key":"7_CR11","unstructured":"Huang, J., Rajagopalan, A.K.: What\u2019s the optimal performance of precise dynamic race detection? - a redundancy perspective. In: ECOOP (2017)"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Huang, J., Zhang, C., Dolby, J.: CLAP: recording local executions to reproduce concurrency failures. In: PLDI 2013. ACM (2013)","DOI":"10.1145\/2491956.2462167"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Kasikci, B., Zamfir, C., Candea, G.: Data races vs. data race bugs: telling the difference with portend. In: ASPLOS 2012. ACM (2012)","DOI":"10.1145\/2150976.2150997"},{"key":"7_CR14","unstructured":"Killian, C., Anderson, J.W., Jhala, R., Vahdat, A.: Life, death, and the critical transition: finding liveness bugs in systems code. In: NSDI 2007. USENIX Association (2007)"},{"key":"7_CR15","unstructured":"Lamport, L.: The TLA+ home page. \nhttps:\/\/lamport.azurewebsites.net\/tla\/tla.html\n\n. Accessed 10 Oct 2019"},{"issue":"7","key":"7_CR16","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)","journal-title":"Commun. ACM"},{"key":"7_CR17","unstructured":"Leesatapornwongsa, T., Hao, M., Joshi, P., Lukman, J.F., Gunawi, H.S.: SAMC: semantic-aware model checking for fast discovery of deep bugs in cloud systems. In: OSDI 2014. USENIX Association (2014)"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Leesatapornwongsa, T., Lukman, J.F., Lu, S., Gunawi, H.S.: TaxDC: a taxonomy of non-deterministic concurrency bugs in datacenter distributed systems. In: ASPLOS 2016. ACM (2016)","DOI":"10.1145\/2872362.2872374"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Li, G., Lu, S., Musuvathi, M., Nath, S., Padhye, R.: Efficient scalable thread-safety-violation detection: finding thousands of concurrency bugs during testing. In: SOSP 2019. ACM (2019)","DOI":"10.1145\/3341301.3359638"},{"issue":"2","key":"7_CR20","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1145\/3093315.3037735","volume":"51","author":"H Liu","year":"2017","unstructured":"Liu, H., et al.: DCatch: automatically detecting distributed concurrency bugs in cloud systems. SIGOPS Oper. Syst. Rev. 51(2), 677\u2013691 (2017)","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"7_CR21","unstructured":"Machado, N., Maia, F., Neves, F., Coelho, F., Pereira, J.: Minha: large-scale distributed systems testing made practical. In: OPODIS 2019. Leibniz International Proceedings in Informatics (LIPIcs) (2019)"},{"key":"7_CR22","unstructured":"Machado, N.: TaxDC Micro-benchmarks Repository (2018). \nhttps:\/\/github.com\/jcp19\/micro-benchmarks"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Machado, N., Lucia, B., Rodrigues, L.: Concurrency debugging with differential schedule projections. In: PLDI 2015. ACM (2015)","DOI":"10.1145\/2737924.2737973"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Machado, N., Lucia, B., Rodrigues, L.: Production-guided concurrency debugging. In: PPoPP 2016. ACM (2016)","DOI":"10.1145\/2851141.2851149"},{"key":"7_CR25","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). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Neves, F., Machado, N., Pereira, J.: Falcon: a practical log-based analysis tool for distributed systems. In: DSN 2018 (2018)","DOI":"10.1109\/DSN.2018.00061"},{"issue":"6","key":"7_CR27","doi-asserted-by":"publisher","first-page":"614","DOI":"10.1145\/2980983.2908118","volume":"51","author":"O Padon","year":"2016","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. SIGPLAN Not. 51(6), 614\u2013630 (2016). \nhttps:\/\/doi.org\/10.1145\/2980983.2908118","journal-title":"SIGPLAN Not."},{"key":"7_CR28","unstructured":"Popper, N.: The stock market bell rings, computers fail, wall street cringes (2015). \nhttps:\/\/www.nytimes.com\/2015\/07\/09\/business\/dealbook\/new-york-stock-exchange-suspends-trading.html\n\n. Accessed 06 Aug 2019"},{"key":"7_CR29","unstructured":"Simsa, J., Bryant, R., Gibson, G.: DBug: Systematic evaluation of distributed systems. In: Proceedings of the 5th International Conference on Systems Software Verification, SSV 2010, p. 3. USENIX Association, Berkeley (2010)"},{"key":"7_CR30","unstructured":"SMT-LIB: Logics. \nhttp:\/\/smtlib.cs.uiowa.edu\/logics.shtml"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Terra-Neves, M., Machado, N., Lynce, I., Manquinho, V.: Concurrency debugging with MaxSMT. In: AAAI 2019. AAAI Press (2019)","DOI":"10.1609\/aaai.v33i01.33011608"},{"key":"7_CR32","unstructured":"Summary of the Amazon EC2 and Amazon RDS Service Disruption in the US East Region (2011). \nhttps:\/\/aws.amazon.com\/message\/65648\/\n\n. Accessed 03 Mar 2019"},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-319-67531-2_17","volume-title":"Runtime Verification","author":"V Tekken Valapil","year":"2017","unstructured":"Tekken Valapil, V., Yingchareonthawornchai, S., Kulkarni, S., Torng, E., Demirbas, M.: Monitoring partially synchronous distributed systems using SMT solvers. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 277\u2013293. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-67531-2_17"},{"issue":"2","key":"7_CR34","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/s10922-005-4441-x","volume":"13","author":"S Voulgaris","year":"2005","unstructured":"Voulgaris, S., Gavidia, D., van Steen, M.: CYCLON: inexpensive membership management for unstructured P2P overlays. J. Netw. Syst. Manag. 13(2), 197\u2013217 (2005)","journal-title":"J. Netw. Syst. Manag."},{"key":"7_CR35","doi-asserted-by":"crossref","unstructured":"Wilcox, J.R., et al.: Verdi: A framework for implementing and formally verifying distributed systems. In: PLDI 2015. ACM (2015)","DOI":"10.1145\/2737924.2737958"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"Woos, D., Wilcox, J.R., Anton, S., Tatlock, Z., Ernst, M.D., Anderson, T.: Planning for change in a formal verification of the Raft consensus protocol. In: CPP 2016. ACM (2016)","DOI":"10.1145\/2854065.2854081"},{"key":"7_CR37","unstructured":"Yang, J., et al.: MODIST: transparent model checking of unmodified distributed systems. In: NSDI 2009. USENIX Association (2009)"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-50995-8_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,19]],"date-time":"2020-06-19T23:06:02Z","timestamp":1592607962000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-50995-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030509941","9783030509958"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-50995-8_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"20 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TAP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tests and Proofs","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bergen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Norway","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 June 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 June 2020","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":"tap2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tap.sosy-lab.org\/2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}