{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:39:15Z","timestamp":1775054355531,"version":"3.50.1"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030374860","type":"print"},{"value":"9783030374877","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-37487-7_20","type":"book-chapter","created":{"date-parts":[[2019,12,13]],"date-time":"2019-12-13T09:22:10Z","timestamp":1576228930000},"page":"232-242","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Towards Automatic Deductive Verification of C Programs over Linear Arrays"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9387-6735","authenticated-orcid":false,"given":"Dmitry","family":"Kondratyev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2497-6484","authenticated-orcid":false,"given":"Ilya","family":"Maryasov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1364-5281","authenticated-orcid":false,"given":"Valery","family":"Nepomniaschy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,12,16]]},"reference":[{"issue":"7","key":"20_CR1","doi-asserted-by":"publisher","first-page":"485","DOI":"10.3103\/S0146411611070029","volume":"45","author":"IS Anureev","year":"2011","unstructured":"Anureev, I.S., Maryasov, I.V., Nepomniaschy, V.A.: C-programs verification based on mixed axiomatic semantics. Autom. Control Comput. Sci. 45(7), 485\u2013500 (2011)","journal-title":"Autom. Control Comput. Sci."},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., et al.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_2"},{"key":"20_CR3","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1017\/S0962492912000050","volume":"21","author":"JJ Dongarra","year":"2012","unstructured":"Dongarra, J.J., van der Steen, A.J.: High-performance computing systems: status and outlook. Acta Numerica 21, 379\u2013474 (2012)","journal-title":"Acta Numerica"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J-C Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 15\u201329. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30482-1_10"},{"issue":"10","key":"20_CR5","doi-asserted-by":"publisher","first-page":"1019","DOI":"10.1109\/TSE.2015.2431688","volume":"41","author":"JP Galeotti","year":"2015","unstructured":"Galeotti, J.P., Furia, C.A., May, E., Fraser, G., Zeller, A.: Inferring loop invariants by mutation, dynamic analysis, and static checking. IEEE Trans. Softw. Eng. 41(10), 1019\u20131037 (2015)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-030-23250-4_9","volume-title":"Intelligent Computer Mathematics","author":"M Johansson","year":"2019","unstructured":"Johansson, M.: Lemma discovery for induction. In: Kaliszyk, C., Brady, E., Kohlhase, A., Sacerdoti Coen, C. (eds.) CICM 2019. LNCS (LNAI), vol. 11617, pp. 125\u2013139. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-23250-4_9"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-319-74313-4_17","volume-title":"Perspectives of System Informatics","author":"D Kondratyev","year":"2018","unstructured":"Kondratyev, D.: Implementing the symbolic method of verification in the C-light project. In: Petrenko, A.K., Voronkov, A. (eds.) PSI 2017. LNCS, vol. 10742, pp. 227\u2013240. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-74313-4_17"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Kondratyev, D.A., Maryasov, I.V., Nepomniaschy, V.A.: The automation of C program verification by symbolic method of loop invariants elimination. Autom. Control Comput. Sci. 53(7) (2019, to appear)","DOI":"10.3103\/S0146411619070101"},{"key":"20_CR9","first-page":"31","volume":"14","author":"DA Kondratyev","year":"2019","unstructured":"Kondratyev, D.A., Promsky, A.V.: Towards automated error localization in C programs with loops. Syst. Inform. 14, 31\u201344 (2019)","journal-title":"Syst. Inform."},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-33693-0_2","volume-title":"Integrated Formal Methods","author":"L Kov\u00e1cs","year":"2016","unstructured":"Kov\u00e1cs, L.: Symbolic computation and automated reasoning for program analysis. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 20\u201327. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_2"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Li, J., Sun, J., Li, L., Le, Q. L., Lin, S.-W.: Automatic loop invariant generation and refinement through selective sampling. In: Proceedings on ASE 2017, pp. 782\u2013792. Conference Publishing Consulting, Passau (2017)","DOI":"10.1109\/ASE.2017.8115689"},{"issue":"6","key":"20_CR12","doi-asserted-by":"publisher","first-page":"773","DOI":"10.18255\/1818-1015-2015-6-773-782","volume":"22","author":"IV Maryasov","year":"2015","unstructured":"Maryasov, I.V., Nepomniaschy, V.A.: Loop invariants elimination for definite iterations over unchangeable data structures in C programs. Model. Anal. Inform. Syst. 22(6), 773\u2013782 (2015)","journal-title":"Model. Anal. Inform. Syst."},{"issue":"6","key":"20_CR13","doi-asserted-by":"publisher","first-page":"743","DOI":"10.18255\/1818-1015-2017-6-743-754","volume":"24","author":"IV Maryasov","year":"2017","unstructured":"Maryasov, I.V., Nepomniaschy, V.A., Kondratyev, D.A.: Invariant elimination of definite iterations over arrays in C programs verification. Model. Anal. Inf. Syst. 24(6), 743\u2013754 (2017)","journal-title":"Model. Anal. Inf. Syst."},{"issue":"7","key":"20_CR14","doi-asserted-by":"publisher","first-page":"407","DOI":"10.3103\/S0146411614070141","volume":"48","author":"IV Maryasov","year":"2014","unstructured":"Maryasov, I.V., Nepomniaschy, V.A., Promsky, A.V., Kondratyev, D.A.: Automatic C program verification based on mixed axiomatic semantics. Autom. Control Comput. Sci. 48(7), 407\u2013414 (2014)","journal-title":"Autom. Control Comput. Sci."},{"issue":"6","key":"20_CR15","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1007\/s00165-019-00490-3","volume":"31","author":"J. Strother Moore","year":"2019","unstructured":"Moore, J.S.: Milestones from the Pure Lisp theorem prover to ACL2. Formal Aspects of Computing, pp. 1\u201334 (2019)","journal-title":"Formal Aspects of Computing"},{"issue":"1","key":"20_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11086-005-0001-0","volume":"31","author":"VA Nepomniaschy","year":"2005","unstructured":"Nepomniaschy, V.A.: Symbolic method of verification of definite iterations over altered data structures. Program. Comput. Softw. 31(1), 1\u20139 (2005)","journal-title":"Program. Comput. Softw."},{"issue":"5\u20136","key":"20_CR17","first-page":"497","volume":"15","author":"S Srivastava","year":"2012","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: Template-based program verification and program synthesis. Int. J. Softw. Tools Technol. Transf. 15(5\u20136), 497\u2013518 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"1","key":"20_CR18","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1145\/322169.322185","volume":"27","author":"N Suzuki","year":"1980","unstructured":"Suzuki, N., Jefferson, D.: Verification decidability of Presburger array programs. J. ACM 27(1), 191\u2013205 (1980)","journal-title":"J. ACM"},{"key":"20_CR19","unstructured":"Tuerk, T.: Local reasoning about while-loops. In: Theory Workshop Proceedings on VSTTE 2010, pp. 29\u201339. Heriot-Watt University, Edinburgh (2010)"},{"key":"20_CR20","unstructured":"Verification of Insertion Sorting Program. https:\/\/bitbucket.org\/Kondratyev\/sorting . Accessed 26 Apr 2019"}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-37487-7_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,8]],"date-time":"2022-10-08T11:20:15Z","timestamp":1665228015000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-37487-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030374860","9783030374877"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-37487-7_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"16 December 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"PSI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Andrei Ershov Memorial Conference on Perspectives of System Informatics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Novosibirsk","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Russia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ershov2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/psi.nsc.ru\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}