{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T05:59:51Z","timestamp":1743055191578,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031646256"},{"type":"electronic","value":"9783031646263"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-64626-3_4","type":"book-chapter","created":{"date-parts":[[2024,7,13]],"date-time":"2024-07-13T13:01:58Z","timestamp":1720875718000},"page":"58-72","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["An Approach to\u00a0Improving Reliability of\u00a0Parallel Graph Computation"],"prefix":"10.1007","author":[{"given":"Jin","family":"Cui","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,14]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Malewicz, G., et al.: Pregel: a system for large-scale graph processing. In: Proceedings of the 2010 ACM SIGMOD International Conference on Management of Data, pp. 135\u2013146 (2010)","DOI":"10.1145\/1807167.1807184"},{"key":"4_CR2","unstructured":"http:\/\/hama.apache.org\/index.html"},{"issue":"1","key":"4_CR3","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1080\/08839514.2020.1842111","volume":"35","author":"D-L Chiang","year":"2021","unstructured":"Chiang, D.-L., et al.: Modeling and analysis of Hadoop mapreduce systems for big data using petri nets. Appl. Artif. Intell. 35(1), 80\u2013104 (2021)","journal-title":"Appl. Artif. Intell."},{"issue":"1","key":"4_CR4","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1109\/TR.2020.2999441","volume":"71","author":"N Zhang","year":"2022","unstructured":"Zhang, N., Wang, M., Duan, Z., Tian, C.: Verifying properties of mapreduce-based big data processing. IEEE Trans. Reliab. 71(1), 321\u2013338 (2022)","journal-title":"IEEE Trans. Reliab."},{"issue":"12","key":"4_CR5","doi-asserted-by":"publisher","first-page":"658","DOI":"10.3390\/info14120658","volume":"14","author":"K Fan","year":"2023","unstructured":"Fan, K., Wang, M.: DAG-based formal modeling of with MSVL. Information 14(12), 658 (2023)","journal-title":"Information"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Bornholt, J., et\u00a0al.: Using lightweight formal methods to validate a key-value storage node in Amazon S3. In: Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles, pp. 836\u2013850 (2021)","DOI":"10.1145\/3477132.3483540"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1007\/978-3-031-30820-8_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Chalupa","year":"2023","unstructured":"Chalupa, M., Henzinger, T.A.: Bubaak: runtime monitoring of program verifiers. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13994, pp. 535\u2013540. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_32"},{"key":"4_CR8","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2021.110962","volume":"177","author":"M Chai","year":"2021","unstructured":"Chai, M., Wang, H., Tang, T., Liu, H.: Runtime verification of train control systems with parameterized modal live sequence charts. J. Syst. Softw. 177, 110962 (2021)","journal-title":"J. Syst. Softw."},{"key":"4_CR9","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2017.07.032","volume":"749","author":"K Yang","year":"2018","unstructured":"Yang, K., Duan, Z., et al.: A compiler for MSVL and its applications. Theor. Comput. Sci. 749, 2\u201316 (2018)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Wang, M., Tian, C., et al.: Verifying full regular temporal properties of programs via dynamic program execution. IEEE Trans. Reliab. (2018)","DOI":"10.1109\/TR.2018.2876333"},{"issue":"8","key":"4_CR11","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1145\/79173.79181","volume":"33","author":"LG Valiant","year":"1990","unstructured":"Valiant, L.G.: A bridging model for parallel computation. Commun. ACM 33(8), 103\u2013111 (1990)","journal-title":"Commun. ACM"},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1016\/j.tcs.2019.12.038","volume":"809","author":"M Wang","year":"2020","unstructured":"Wang, M., Tian, C., Zhang, N., Duan, Z., Yao, C.: Translating XD-C programs to MSVL programs. Theor. Comput. Sci. 809, 430\u2013465 (2020)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Duan, Z.: Temporal Logic and Temporal Logic Programming. Science Press (2005)","DOI":"10.1007\/11562931_27"},{"key":"4_CR14","doi-asserted-by":"publisher","first-page":"762","DOI":"10.1007\/s11704-016-6059-4","volume":"11","author":"X Wang","year":"2017","unstructured":"Wang, X., Tian, C., Duan, Z., Zhao, L.: MSVL: a typed language for temporal logic programming. Front. Comput. Sci. 11, 762\u2013785 (2017)","journal-title":"Front. Comput. Sci."},{"key":"4_CR15","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/j.tcs.2016.02.037","volume":"654","author":"N Zhang","year":"2016","unstructured":"Zhang, N., Duan, Z., Tian, C.: A mechanism of function calls in MSVL. Theor. Comput. Sci. 654, 11\u201325 (2016)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Navabpour, S., et al.: RiTHM: a tool for enabling time-triggered runtime verification for C programs. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, pp. 603\u2013606 (2013)","DOI":"10.1145\/2491411.2494596"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-662-49674-9_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Brockschmidt","year":"2016","unstructured":"Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 387\u2013393. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_22"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-21690-4_4","volume-title":"Computer Aided Verification","author":"D Dietsch","year":"2015","unstructured":"Dietsch, D., Heizmann, M., Langenfeld, V., Podelski, A.: Fairness modulo theory: a new approach to LTL software model checking. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 49\u201366. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_4"},{"key":"4_CR19","unstructured":"Cadar, C., et\u00a0al.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, vol. 8, pp. 209\u2013224 (2008)"},{"key":"4_CR20","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"},{"issue":"1\u20137","key":"4_CR21","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/S0169-7552(98)00110-X","volume":"30","author":"S Brin","year":"1998","unstructured":"Brin, S., Page, L.: The anatomy of a large-scale hypertextual web search engine. Comput. Netw. ISDN Syst. 30(1\u20137), 107\u2013117 (1998)","journal-title":"Comput. Netw. ISDN Syst."},{"key":"4_CR22","volume":"392","author":"L Tortosa","year":"2021","unstructured":"Tortosa, L., Vicent, J.F., Yeghikyan, G.: An algorithm for ranking the nodes of multiplex networks with data based on the pagerank concept. Appl. Math. Comput. 392, 125676 (2021)","journal-title":"Appl. Math. Comput."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-64626-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,12]],"date-time":"2025-03-12T16:16:28Z","timestamp":1741796188000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-64626-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031646256","9783031646263"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-64626-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"14 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Theoretical Aspects of Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Guiyang","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 August 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tase2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tase2024.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}