{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T23:05:30Z","timestamp":1773615930952,"version":"3.50.1"},"reference-count":30,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T00:00:00Z","timestamp":1764547200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T00:00:00Z","timestamp":1764547200000},"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":[[2025,12]]},"DOI":"10.3103\/s0146411625700361","type":"journal-article","created":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T19:14:55Z","timestamp":1771528495000},"page":"1048-1081","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Pattern-Based Approach to the Automation of Deductive Verification of Process-Oriented Programs: Patterns, Lemmas, and Algorithms"],"prefix":"10.3103","volume":"59","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7675-8449","authenticated-orcid":false,"given":"I. M.","family":"Chernenko","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9574-128X","authenticated-orcid":false,"given":"I.\u00a0S.","family":"Anureev","sequence":"additional","affiliation":[]}],"member":"1627","published-online":{"date-parts":[[2026,2,19]]},"reference":[{"key":"7896_CR1","doi-asserted-by":"publisher","unstructured":"Zyubin, V.E., Hyper-automaton: A model of control algorithms, 2007 Siberian Conference on Control and Communications, Tomsk, 2007, IEEE, 2007, pp. 51\u201357. https:\/\/doi.org\/10.1109\/sibcon.2007.371297","DOI":"10.1109\/sibcon.2007.371297"},{"key":"7896_CR2","doi-asserted-by":"publisher","first-page":"35238","DOI":"10.1109\/ACCESS.2022.3157601","volume":"10","author":"V.E. Zyubin","year":"2022","unstructured":"Zyubin, V.E., Rozov, A.S., Anureev, I.S., Garanina, N.O., and Vyatkin, V., poST: A process-oriented extension of the IEC 61131-3 structured text language, IEEE Access, 2022, vol. 10, pp. 35238\u201335250. https:\/\/doi.org\/10.1109\/ACCESS.2022.3157601","journal-title":"IEEE Access"},{"key":"7896_CR3","unstructured":"IEC 61131-3: 2013 Programmable Controllers. Part 3: Programming languages, 2013. https:\/\/webstore.iec.ch\/publication\/4552."},{"key":"7896_CR4","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R. and Huisman, M., Deductive software verification: From pen-and-paper proofs to industrial tools, Computing and Software Science, Steffen, B. and Woeginger, G., Eds., Lecture Notes in Computer Science, vol. 10000, Cham: Springer, 2019, pp. 345\u2013373. https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18","DOI":"10.1007\/978-3-319-91908-9_18"},{"key":"7896_CR5","doi-asserted-by":"publisher","unstructured":"Anureev, I., Garanina, N., Liakh, T., Rozov, A., Zyubin, V., and Gorlatch, S., Two-step deductive verification of control software using reflex, Perspectives of System Informatics. PSI 2019, Bj\u00f8rner, N., Virbitskaite, I., and Voronkov, A., Eds., Lecture Notes in Computer Science, vol. 11964, Cham: Springer, 2019, pp. 50\u201363. https:\/\/doi.org\/10.1007\/978-3-030-37487-7_5","DOI":"10.1007\/978-3-030-37487-7_5"},{"key":"7896_CR6","doi-asserted-by":"publisher","unstructured":"Chernenko, I., Anureev, I.S., Garanina, N.O., and Staroletov, S.M., A temporal requirements language for deductive verification of process-oriented programs, Proceedings of the IEEE 23rd International Conference of Young Professionals in Electron Devices and Materials (EDM), IEEE, 2022, pp. 657\u2013662. https:\/\/doi.org\/10.1109\/EDM55285.2022.9855145","DOI":"10.1109\/EDM55285.2022.9855145"},{"key":"7896_CR7","doi-asserted-by":"publisher","unstructured":"Chernenko, I., Requirements patterns in deductive verification of process-oriented programs and examples of their use, Sistemnaya Informatika, 2023, no. 22, pp. 11\u201320. https:\/\/doi.org\/10.31144\/si.2307-6410.2023.n22.p11-20","DOI":"10.31144\/si.2307-6410.2023.n22.p11-20"},{"key":"7896_CR8","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/s00165-019-00492-1","volume":"31","author":"L.C. Paulson","year":"2019","unstructured":"Paulson, L.C., Nipkow, T., and Wenzel, M., From LCF to Isabelle\/HOL, Formal Aspects Comput., 2019, vol. 31, no. 6, pp. 675\u2013698. https:\/\/doi.org\/10.1007\/s00165-019-00492-1","journal-title":"Formal Aspects Comput."},{"key":"7896_CR9","doi-asserted-by":"publisher","unstructured":"Handbook of Model Checking, Clarke, E.M., Henzinger, T.A., Veith, H., and Bloem, R., Eds., Cham: Springer, 2018. https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"7896_CR10","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10817-015-9360-2","volume":"56","author":"D. Matichuk","year":"2016","unstructured":"Matichuk, D., Murray, T., and Wenzel, M., Eisbach: A proof method language for Isabelle, J. Autom. Reasoning, 2016, vol. 56, no. 3, pp. 261\u2013282. https:\/\/doi.org\/10.1007\/s10817-015-9360-2","journal-title":"J. Autom. Reasoning"},{"key":"7896_CR11","doi-asserted-by":"publisher","first-page":"1003","DOI":"10.3103\/s0146411624700421","volume":"58","author":"I.M. Chernenko","year":"2024","unstructured":"Chernenko, I.M., Anureev, I.S., and Garanina, N.O., Requirement patterns in deductive verification of poST programs, Autom. Control Comput. Sci., 2024, vol. 58, no. 7, pp. 1003\u20131024. https:\/\/doi.org\/10.3103\/s0146411624700421","journal-title":"Autom. Control Comput. Sci."},{"key":"7896_CR12","doi-asserted-by":"publisher","unstructured":"Cousot, P. and Cousot, R., Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, Los Angeles, 1977, New York: Association for Computing Machinery, 1977, pp. 238\u2013252. https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"7896_CR13","doi-asserted-by":"publisher","unstructured":"Suzuki, N. and Ishihata, K., Implementation of an array bound checker, Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages\u2014POPL \u201977, Los Angeles, 1977, New York: Association for Computing Machinery, 1977, pp. 132\u2013143. https:\/\/doi.org\/10.1145\/512950.512963","DOI":"10.1145\/512950.512963"},{"key":"7896_CR14","doi-asserted-by":"publisher","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., and Sipma, H.B., Linear invariant generation using non-linear constraint solving, Computer Aided Verification, Hunt, W.A. and Somenzi, F., Eds., Lecture Notes in Computer Science, vol. 2725, Berlin: Springer, 2003, pp. 420\u2013432. https:\/\/doi.org\/10.1007\/978-3-540-45069-6_39","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"7896_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Reasoning algebraically about P-solvable loops, Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2008","author":"L. Kov\u00e1cs","year":"2008","unstructured":"Kov\u00e1cs, L., Reasoning algebraically about P-solvable loops, Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2008, Ramakrishnan, C.R. and Rehof, J., Eds., Lecture Notes in Computer Science, vol.\u00a04963, Berlin: Springer, 2008, pp. 249\u2013264."},{"key":"7896_CR16","doi-asserted-by":"publisher","unstructured":"Stark, J. and Ireland, A., Invariant discovery via failed proof attempts, Logic-Based Program Synthesis and Transformation. LOPSTR 1998, Flener, P., Ed., Lecture Notes in Computer Science, vol. 1559, Berlin: Springer, 1998, pp. 271\u2013288. https:\/\/doi.org\/10.1007\/3-540-48958-4_15","DOI":"10.1007\/3-540-48958-4_15"},{"key":"7896_CR17","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M. and Logozzo, F., Loop invariants on demand, Programming Languages and Systems. APLAS 2005, Yi, K., Ed., Lecture Notes in Computer Science, vol. 3780, Berlin: Springer, 2005, pp. 119\u2013134. https:\/\/doi.org\/10.1007\/11575467_9","DOI":"10.1007\/11575467_9"},{"key":"7896_CR18","doi-asserted-by":"publisher","unstructured":"Ernst, M.D., Cockrell, J., Griswold, W.G., and Notkin, D., Dynamically discovering likely program invariants to support program evolution, Proceedings of the 21st International Conference on Software Engineering, Los Angeles, 1999, New York: Association for Computing Machinery, 1999, pp. 213\u2013224. https:\/\/doi.org\/10.1145\/302405.302467","DOI":"10.1145\/302405.302467"},{"key":"7896_CR19","unstructured":"Si, X., Dai, H., Raghothaman, M., Naik, M., and Song, L., Learning loop invariants for program verification, Adv. Neural Inf. Process. Syst., 2018, vol. 31."},{"key":"7896_CR20","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1145\/2506375","volume":"46","author":"C.A. Furia","year":"2014","unstructured":"Furia, C.A., Meyer, B., and Velder, S., Loop invariants: Analysis, classification, and examples, ACM Comput. Surv., 2014, vol. 46, no. 3, p. 34. https:\/\/doi.org\/10.1145\/2506375","journal-title":"ACM Comput. Surv."},{"key":"7896_CR21","doi-asserted-by":"publisher","unstructured":"Breck, J., Cyphert, J., Kincaid, Z., and Reps, T., Templates and recurrences: Better together, Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, London, 2020, New York: Association for Computing Machinery, 2020, pp. 688\u2013702. https:\/\/doi.org\/10.1145\/3385412.3386035","DOI":"10.1145\/3385412.3386035"},{"key":"7896_CR22","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/s10009-012-0223-4","volume":"15","author":"S. Srivastava","year":"2013","unstructured":"Srivastava, S., Gulwani, S., and Foster, J.S., Template-based program verification and program synthesis, Int. J. Software Tools Technol. Transfer, 2013, vol. 15, nos. 5\u20136, pp. 497\u2013518. https:\/\/doi.org\/10.1007\/s10009-012-0223-4","journal-title":"Int. J. Software Tools Technol. Transfer"},{"key":"7896_CR23","doi-asserted-by":"crossref","unstructured":"Manna, Z., Bj\u00f8rner, N., Browne, A., Chang, E.Y., Col\u00f3n, M., Alfaro, L.d., Devarajan, H., Kapur, A., Lee, J., Sipma, H., and Uribe, T.E., STeP: The Stanford temporal prover, Proceedings of the TAPSOFT\u201995: Theory and Practice of Software Development, Springer, 1995, pp. 793\u2013794.","DOI":"10.1007\/3-540-59293-8_237"},{"key":"7896_CR24","doi-asserted-by":"publisher","first-page":"977","DOI":"10.1007\/s10009-022-00680-0","volume":"24","author":"C. Belo Louren\u00e7o","year":"2022","unstructured":"Belo Louren\u00e7o, C., Cousineau, D., Faissole, F., March\u00e9, C., Mentr\u00e9, D., and Inoue, H., Automated formal analysis of temporal properties of Ladder programs, Int. J. Software Tools Technol. Transfer, 2022, vol. 24, no. 6, pp. 977\u2013997. https:\/\/doi.org\/10.1007\/s10009-022-00680-0","journal-title":"Int. J. Software Tools Technol. Transfer"},{"key":"7896_CR25","doi-asserted-by":"publisher","unstructured":"Blanchard, A., Loulergue, F., and Kosmatov, N., Towards full proof automation in Frama-C using auto-active verification, NASA Formal Methods. NFM 2019, Badger, J. and Rozier, K., Eds., Lecture Notes in Computer Science, vol. 11460, Cham: Springer, 2019, pp. 88\u2013105. https:\/\/doi.org\/10.1007\/978-3-030-20652-9_6","DOI":"10.1007\/978-3-030-20652-9_6"},{"key":"7896_CR26","doi-asserted-by":"publisher","unstructured":"Naumchev, A., Seamless object-oriented requirements, 2019 International Multi-Conference on Engineering, Computer and Information Sciences (SIBIRCON), Novosibirsk, 2019, IEEE, 2019, pp. 743\u2013748. https:\/\/doi.org\/10.1109\/SIBIRCON48586.2019.8958211","DOI":"10.1109\/SIBIRCON48586.2019.8958211"},{"key":"7896_CR27","doi-asserted-by":"publisher","unstructured":"Gupta, A. and Rybalchenko, A., InvGen: An efficient invariant generator, Computer Aided Verification. CAV 2009, Bouajjani, A. and Maler, O., Eds., Lecture Notes in Computer Science, vol. 5643, Berlin: Springer, 2009, pp. 634\u2013640. https:\/\/doi.org\/10.1007\/978-3-642-02658-4_48","DOI":"10.1007\/978-3-642-02658-4_48"},{"key":"7896_CR28","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., and Rybalchenko, A., Invariant synthesis for combined theories, 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. 378\u2013394. https:\/\/doi.org\/10.1007\/978-3-540-69738-1_27","DOI":"10.1007\/978-3-540-69738-1_27"},{"key":"7896_CR29","unstructured":"Mekki, A., Ghazel, M., and Toguyeni, A., Patterns-based assistance for temporal requirement specification, Proceedings of the International Conference on Software Engineering Research and Practice (SERP), Las Vegas, 2011, CSREA Press, 2011, pp. 578\u2013584."},{"key":"7896_CR30","doi-asserted-by":"publisher","unstructured":"Dwyer, M.B., Avrunin, G.S., and Corbett, J.C., Patterns in property specifications for finite-state verification, Proceedings of the 21st International Conference on Software Engineering, Los Angeles, 1999, New York: Association for Computing Machinery, 1999, pp. 411\u2013420. https:\/\/doi.org\/10.1145\/302405.302672","DOI":"10.1145\/302405.302672"}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411625700361.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411625700361","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411625700361.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:07:26Z","timestamp":1773612446000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411625700361"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,12]]},"references-count":30,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["7896"],"URL":"https:\/\/doi.org\/10.3103\/s0146411625700361","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,12]]},"assertion":[{"value":"6 November 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 November 2024","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 November 2024","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 February 2026","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The authors of this work declare that they have no conflicts of interest.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"CONFLICT OF INTEREST"}}]}}