{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:06:42Z","timestamp":1773655602353,"version":"3.50.1"},"reference-count":15,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2019,12,1]],"date-time":"2019-12-01T00:00:00Z","timestamp":1575158400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2019,12,1]],"date-time":"2019-12-01T00:00:00Z","timestamp":1575158400000},"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":[[2019,12]]},"DOI":"10.3103\/s0146411619070101","type":"journal-article","created":{"date-parts":[[2020,3,4]],"date-time":"2020-03-04T10:02:40Z","timestamp":1583316160000},"page":"653-662","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["The Automation of C Program Verification by the Symbolic Method of Loop Invariant Elimination"],"prefix":"10.3103","volume":"53","author":[{"given":"D. A.","family":"Kondratyev","sequence":"first","affiliation":[]},{"given":"I. V.","family":"Maryasov","sequence":"additional","affiliation":[]},{"given":"V. A.","family":"Nepomniaschy","sequence":"additional","affiliation":[]}],"member":"1627","published-online":{"date-parts":[[2020,3,4]]},"reference":[{"key":"7166_CR1","doi-asserted-by":"publisher","first-page":"485","DOI":"10.3103\/S0146411611070029","volume":"45","author":"I.S. Anureev","year":"2011","unstructured":"Anureev, I.S., Maryasov, I.V., and Nepomniaschy, V.A., C-programs verification based on mixed axiomatic semantics, Autom. Control Comput. Sci., 2011, vol. 45, no. 7, pp. 485\u2013500.","journal-title":"Autom. Control Comput. Sci."},{"key":"7166_CR2","doi-asserted-by":"crossref","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., and Tobies, S., VCC: A practical system for verifying concurrent C, 22nd Int. Conf. TPHOLs; Lect. Notes Comput. Sci., 2009, vol. 5674, pp. 23\u201342.","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"7166_CR3","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1017\/S0962492912000050","volume":"21","author":"J.J. Dongarra","year":"2012","unstructured":"Dongarra, J.J. and van der Steen, A.J., High-performance computing systems: Status and outlook, Acta Numer., 2012, vol. 21, pp. 379\u2013474.","journal-title":"Acta Numer."},{"key":"7166_CR4","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume":"3308","author":"J.-C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C. and March\u00e9, C., Multi-prover verification of C programs, 6th ICFEM,Lect. Notes Comput. Sci., 2004, vol. 3308, pp. 15\u201329.","journal-title":"Lect. Notes Comput. Sci."},{"key":"7166_CR5","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-39656-7_8","volume":"2852","author":"B. Jacobs","year":"2003","unstructured":"Jacobs, B., Kiniry, J.L., and Warnier, M., Java program verification challenges, FMCO 2002; Lect. Notes Comput. Sci., 2003, vol. 2852, pp. 202\u2013219.","journal-title":"Lect. Notes Comput. Sci."},{"key":"7166_CR6","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/32.588534","volume":"23","author":"M. Kaufmann","year":"1997","unstructured":"Kaufmann, M. and Moore, J.S., An industrial strength theorem prover for a logic based on common Lisp, IEEE Trans. Software Eng., 1997, vol. 23, no. 4, pp. 203\u2013213.","journal-title":"IEEE Trans. Software Eng."},{"key":"7166_CR7","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-319-74313-4_17","volume":"10742","author":"D. Kondratyev","year":"2018","unstructured":"Kondratyev, D., Implementing the symbolic method of verification in the C-Light project, PSI 2017; Lect. Notes Comput. Sci., 2018, vol. 10742, pp. 227\u2013240.","journal-title":"Lect. Notes Comput. Sci."},{"key":"7166_CR8","unstructured":"Kondratyev, D.A., Towards loop invariant elimination for definite iterations over changeable data structures in C programs verification. Appendices. https:\/\/bitbucket.org\/c-light\/loop-invariant-elimination."},{"key":"7166_CR9","unstructured":"Kondratyev, D.A., Maryasov, I.V., and Nepomniaschy, V.A., Towards loop invariant elimination for definite iterations over changeable data structures in C programs verification, PSSV 2018, Workshop Proceedings, Yaroslavl, 2018, pp. 51\u201357."},{"key":"7166_CR10","doi-asserted-by":"crossref","unstructured":"Li, J., Sun, J., Li, L., Loc, Le Q., and Lin, S.-W., Automatic loop invariant generation and refinement through selective sampling, 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE), 2017, pp. 782\u2013792.","DOI":"10.1109\/ASE.2017.8115689"},{"key":"7166_CR11","doi-asserted-by":"publisher","first-page":"773","DOI":"10.18255\/1818-1015-2015-6-773-782","volume":"22","author":"I.V. Maryasov","year":"2015","unstructured":"Maryasov, I.V. and Nepomniaschy, V.A., Loop invariants elimination for definite iterations over unchangeable data structures in C programs, Model. Anal. Inf. Syst., 2015, vol. 22, no. 6, pp. 773\u2013782.","journal-title":"Model. Anal. Inf. Syst."},{"key":"7166_CR12","doi-asserted-by":"publisher","first-page":"743","DOI":"10.18255\/1818-1015-2017-6-743-754","volume":"24","author":"I.V. Maryasov","year":"2017","unstructured":"Maryasov, I.V., Nepomniaschy, V.A., and Kondratyev, D.A., Invariant elimination of definite iterations over arrays in C programs verification, Model. Anal. Inf. Syst., 2017, vol. 24, no. 6, pp. 743\u2013754.","journal-title":"Model. Anal. Inf. Syst."},{"key":"7166_CR13","doi-asserted-by":"publisher","first-page":"407","DOI":"10.3103\/S0146411614070141","volume":"48","author":"I.V. Maryasov","year":"2014","unstructured":"Maryasov, I.V., Nepomniaschy, V.A., Promsky, A.V., and Kondratyev, D.A., Automatic C program verification based on mixed axiomatic semantics, Autom. Control Comput. Sci., 2014, vol. 48, no. 7, pp. 407\u2013414.","journal-title":"Autom. Control Comput. Sci."},{"key":"7166_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11086-005-0001-0","volume":"31","author":"V.A. Nepomniaschy","year":"2005","unstructured":"Nepomniaschy, V.A., Symbolic method of verification of definite iterations over altered data structures, Program. Comput. Software, 2005, vol. 31, no. 1, pp. 1\u20139.","journal-title":"Program. Comput. Software"},{"key":"7166_CR15","unstructured":"Tuerk, T., Local reasoning about while-loops, VSTTE 2010, Workshop Proceedings, 2010, pp. 29\u201339."}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411619070101.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411619070101","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411619070101.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T21:59:21Z","timestamp":1773611961000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411619070101"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12]]},"references-count":15,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2019,12]]}},"alternative-id":["7166"],"URL":"https:\/\/doi.org\/10.3103\/s0146411619070101","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12]]},"assertion":[{"value":"10 September 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 March 2020","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The authors declare that they have no conflicts of interest.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"CONFLICT OF INTEREST"}}]}}