{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T23:01:41Z","timestamp":1773615701272,"version":"3.50.1"},"reference-count":12,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"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":["Aut. Control Comp. Sci."],"published-print":{"date-parts":[[2022,12]]},"DOI":"10.3103\/s014641162207015x","type":"journal-article","created":{"date-parts":[[2023,2,19]],"date-time":"2023-02-19T09:03:26Z","timestamp":1676797406000},"page":"762-777","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Mathematical Model of Parallel Programs and an Approach to Verification of MPI Programs Based on the Proposed Model"],"prefix":"10.3103","volume":"56","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9132-7804","authenticated-orcid":false,"given":"A. M.","family":"Mironov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1627","published-online":{"date-parts":[[2023,2,19]]},"reference":[{"key":"7530_CR1","volume-title":"Design and Validation of Computer Protocols","author":"G.J. Holzmann","year":"1990","unstructured":"Holzmann, G.J., Design and Validation of Computer Protocols, Prentice-Hall, 1990."},{"key":"7530_CR2","doi-asserted-by":"publisher","unstructured":"Lopez, H.A., Marques, E.R., Martins, F., Ng, N., Santos, C., Vasconcelos, V.T., and Yoshida, N., Protocol-based verification of message-passing parallel programs, OOPSLA 2015: Proc. 2015 ACM SIGPLAN Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications, Pittsburgh, Pa., 2015, New York: Association for Computing Machinery, 2015, pp. 280\u2013298. \u00a0https:\/\/doi.org\/10.1145\/2814270.2814302","DOI":"10.1145\/2814270.2814302"},{"key":"7530_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11846802_23","volume-title":"Modeling and verification of MPI based distributed software, Recent Advances in Parallel Virtual Machine and Message Passing Interface. EuroPVM\/MPI 2006","author":"I. Grudenic","year":"2006","unstructured":"Grudenic, I. and Bogunovic, N., Modeling and verification of MPI based distributed software, Recent Advances in Parallel Virtual Machine and Message Passing Interface. EuroPVM\/MPI 2006, Mohr, B., Tr\u00e4ff, J.L., Worringen, J., and Dongarra, J., Eds., Lecture Notes in Computer Science, vol. 4192, Berlin: Springer, 2006, pp. 123\u2013132. \u00a0https:\/\/doi.org\/10.1007\/11846802_23"},{"key":"7530_CR4","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1145\/937555.937561","volume":"4","author":"A. Blass","year":"2003","unstructured":"Blass, A. and Gurevich, Yu., Abstract state machines capture parallel algorithms, ACM Trans. Comput. Logic, 2003, vol. 4, no. 4, pp. 578\u2013651. \u00a0https:\/\/doi.org\/10.1145\/937555.937561","journal-title":"ACM Trans. Comput. Logic"},{"key":"7530_CR5","doi-asserted-by":"publisher","unstructured":"Siegel, S.F., Model checking nonblocking MPI programs, International Workshop on Verification, Model Checking, and Abstract Interpretation, VMCAI 2007, Cook, B. and Podelski, A., Eds., Lecture Notes in Computer Science, vol. 4349, Berlin: Springer, 2007, pp.\u00a044\u201358. \u00a0https:\/\/doi.org\/10.1007\/978-3-540-69738-1_3","DOI":"10.1007\/978-3-540-69738-1_3"},{"key":"7530_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1348250.1348256","volume":"17","author":"S.F. Siegel","year":"2008","unstructured":"Siegel, S.F., Mironova, A., Avrunin, G.S., and Clarke, L.A., Combining symbolic execution with model checking to verify parallel numerical programs, ACM Trans. Software Eng. Methodol., 2008, vol. 17, no. 2, pp. 1\u201334. \u00a0https:\/\/doi.org\/10.1145\/1348250.1348256","journal-title":"ACM Trans. Software Eng. Methodol."},{"key":"7530_CR7","doi-asserted-by":"publisher","unstructured":"Vakkalanka, S., Gopalakrishnan, G., and Kirby, R.M., Dynamic verification of MPI programs with reductions in presence of split operations and relaxed orderings, International Conference on Computer Aided Verification. CAV 2008, Gupta, A. and Malik, S., Eds., Lecture Notes in Computer Science, vol. 5123, Berlin: Springer, 2008, pp. 66\u201379. \u00a0https:\/\/doi.org\/10.1007\/978-3-540-70545-1_9","DOI":"10.1007\/978-3-540-70545-1_9"},{"key":"7530_CR8","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/2043174.2043194","volume":"54","author":"G. Gopalakrishnan","year":"2011","unstructured":"Gopalakrishnan, G., Kirby, R.M., Siegel, S., Thakur, R., Gropp, W., Lusk, E., De\u00a0Supinski,\u00a0B.R., Schulz, M., and Bronevetsky, G., Formal analysis of MPI-based parallel programs, Commun. ACM, 2011, vol. 54, no. 12, pp. 82\u201391. \u00a0https:\/\/doi.org\/10.1145\/2043174.2043194","journal-title":"Commun. ACM"},{"key":"7530_CR9","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/3095075","volume":"39","author":"V. Forejt","year":"2017","unstructured":"Forejt, V., Joshi, S., Kroening, D., Narayanaswamy, G., and Sharma, S., Precise predictive analysis for discovering communication deadlocks in MPI programs, ACM Trans. Program. Languages Syst., 2017, vol. 39, no. 4, p. 15. \u00a0https:\/\/doi.org\/10.1145\/3095075","journal-title":"ACM Trans. Program. Languages Syst."},{"key":"7530_CR10","doi-asserted-by":"publisher","DOI":"10.1145\/3127024.3127032","volume-title":"Verification of MPI programs using CIVL, EuroMPI \u201917: Proc. 24th European MPI Users\u2019 Group Meeting, Chicago","author":"Z. Luo","year":"2017","unstructured":"Luo, Z., Zheng, M, and Siegel, S.F, Verification of MPI programs using CIVL, EuroMPI \u201917: Proc. 24th European MPI Users\u2019 Group Meeting, Chicago, 2017, New York: Association for Computing Machinery, 2017, p. 6. \u00a0https:\/\/doi.org\/10.1145\/3127024.3127032"},{"key":"7530_CR11","doi-asserted-by":"publisher","first-page":"200101","DOI":"10.1007\/s11432-018-9825-3","volume":"62","author":"W. Hong","year":"2019","unstructured":"Hong, W., Chen, Z., Yu, H., and Wang, J., Evaluation of model checkers by verifying message passing programs, Sci. China Inf. Sci., 2019, vol. 62, p. 200101. \u00a0https:\/\/doi.org\/10.1007\/s11432-018-9825-3","journal-title":"Sci. China Inf. Sci."},{"key":"7530_CR12","doi-asserted-by":"publisher","unstructured":"Yu, H., Chen, Z., Fu, X., Wang, J., Su, Z., Sun, J., Huang, C., and Dong, W., Symbolic verification of message passing interface programs, ICSE \u201920: Proc. ACM\/IEEE 42nd International Conference on Software Engineering, Seoul, 2020, New York: Association for Computing Machinery, 2020, pp. 1248\u20131260. \u00a0https:\/\/doi.org\/10.1145\/3377811.3380419","DOI":"10.1145\/3377811.3380419"}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S014641162207015X.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S014641162207015X","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S014641162207015X.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:03:29Z","timestamp":1773612209000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S014641162207015X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12]]},"references-count":12,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["7530"],"URL":"https:\/\/doi.org\/10.3103\/s014641162207015x","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,12]]},"assertion":[{"value":"15 November 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 December 2021","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 December 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 February 2023","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The author declares that he has no conflicts of interest.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"CONFLICT OF INTEREST"}}]}}