{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:47:44Z","timestamp":1773654464681,"version":"3.50.1"},"reference-count":16,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2014,12,1]],"date-time":"2014-12-01T00:00:00Z","timestamp":1417392000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,12,1]],"date-time":"2014-12-01T00:00:00Z","timestamp":1417392000000},"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":[[2014,12]]},"DOI":"10.3103\/s0146411614070141","type":"journal-article","created":{"date-parts":[[2015,1,30]],"date-time":"2015-01-30T19:16:45Z","timestamp":1422645405000},"page":"407-414","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Automatic C program verification based on mixed axiomatic semantics"],"prefix":"10.3103","volume":"48","author":[{"given":"I. V.","family":"Maryasov","sequence":"first","affiliation":[]},{"given":"V. A.","family":"Nepomnyaschy","sequence":"additional","affiliation":[]},{"given":"A. V.","family":"Promsky","sequence":"additional","affiliation":[]},{"given":"D. A.","family":"Kondratyev","sequence":"additional","affiliation":[]}],"member":"1627","published-online":{"date-parts":[[2015,2,1]]},"reference":[{"key":"6342_CR1","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"E Gamma","year":"1994","unstructured":"Gamma, E., Helm, R., Johnson, R., and Vlissides, J., Design Patterns: Elements of Reusable Object-Oriented Software, Addison-Wesley, 1994."},{"key":"6342_CR2","first-page":"79","volume-title":"Sist. Inform.","author":"DA Kondratyev","year":"2013","unstructured":"Kondratyev, D.A. and Promsky, A.V., Complex approach to error localization at C-program verification, Sist. Inform., 2013, no. 1, pp. 79\u201396."},{"key":"6342_CR3","first-page":"51","volume-title":"Sistemnaya informatika: Sbornik nauchnykh trudov. Vyp. 9: Formalnye metody i modeli informatiki","author":"VA Nepomnyaschy","year":"2004","unstructured":"Nepomnyaschy, V.A., Anureev, I.S., Mikhaylov, I.N., and Promsky, A.V., C-light language oriented on verification, in Sistemnaya informatika: Sbornik nauchnykh trudov. Vyp. 9: Formalnye metody i modeli informatiki (System Informatics: Coll. Sci. Papers. Part. 9. Formal Methods and Models of Informatics), Novosibirsk: Sibir. Otd. Ross. Akad. Nauk, 2004, pp. 51\u2013134."},{"key":"6342_CR4","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., and Nepomniaschy, V.A., C-programs verification based on mixed axiomatic semantics, Autom. Control Compt. Sci., 2011, vol. 45, pp. 485\u2013500.","journal-title":"Autom. Control Compt. Sci."},{"key":"6342_CR5","first-page":"16","volume-title":"Proc. 3rd Workshop \u201cPSSV: Theory and Applications\u201d Nizhni Novgorod","author":"I Anureev","year":"2012","unstructured":"Anureev, I., Maryasov, I., and Nepomniaschy, V., Revised mixed axiomatic semantics method of C program verification, Proc. 3rd Workshop \u201cPSSV: Theory and Applications\u201d Nizhni Novgorod, 2012, pp. 16\u201323."},{"key":"6342_CR6","unstructured":"Baudin, P., Cuoq, P., Filliatre, J.-C., March\u00e9, C., Monate, B., Moy, Y., and Prevosto, V., ACSL: ANSI\/ISO C Specification Language. http:\/\/frama-c.com\/download\/acsl-1.4.pdf"},{"key":"6342_CR7","first-page":"3","volume":"7421","author":"T Bormer","year":"2011","unstructured":"Bormer, T., Brockschmidt, M., Distefano, D., Ernst, G., Filliatre, J.-C., Grigore, R., Huisman, M., Klebanov, V., March\u00e9, C., Monahan, R., Mostowski, W., Polikarpova, N., Scheben, C., Schellhorn, G., Tofan, B., Tschannen, J., and Ulbrich, M., The COST IC0701 verification competition 2011, Revised Selected Papers of Int. Conf. FoVeOOS, Lect. Notes Compt. Sci., 2011, vol. 7421, pp. 3\u201321.","journal-title":"Revised Selected Papers of Int. Conf. FoVeOOS, Lect. Notes Compt. Sci."},{"key":"6342_CR8","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume":"5674","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., and Tobies, S., VCC: A practical system for verifying voncurrent C, Proc. 22nd Int. Conf. TPHOLs. Lect. Notes Compt. Sci., 2009, vol. 5674, pp. 23\u201342.","journal-title":"Proc. 22nd Int. Conf. TPHOLs. Lect. Notes Compt. Sci."},{"key":"6342_CR9","volume-title":"Simplify: A Theorem Prover for Program Checking. HP Tech. Rep. HPL-2003-148","author":"D Detlefs","year":"2003","unstructured":"Detlefs, D., Nelson, G., and Saxe, J.B., Simplify: A Theorem Prover for Program Checking. HP Tech. Rep. HPL-2003-148, Palo Alto, 2003. http:\/\/www.hpl.hp.com\/techreports\/2003\/HPL-2003-148.pdf"},{"key":"6342_CR10","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume":"3308","author":"J-C Filliatre","year":"2004","unstructured":"Filliatre, J.-C. and March\u00e9, C., Multi-prover verification of C programs, Proc. of 6th ICFEM, Lect. Notes Compt. Sci., 2004, vol. 3308, pp. 15\u201329.","journal-title":"Proc. of 6th ICFEM, Lect. Notes Compt. Sci."},{"key":"6342_CR11","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-21437-0_14","volume":"6664","author":"V Klebanov","year":"2011","unstructured":"Klebanov, V., M\u00fcller, P., Shankar, N., Leavens, G.T., W\u00fcstholz, V., Alkassar, E., Arthan, R., Bronish, D., Chapman, R., Cohen, E., Hillebrand, M., Jacobs, B., Leino, K.R.M., Monahan, R., Piessens, F., Polikarpova, N., Ridge, T., Smans, J., Tobies, S., Tuerk, T., Ulbrich, M., and Wei, B., The 1st verified software competition: Experience report, Proc. 17th Int. Symp. on Formal Methods. Lect. Notes Compt. Sci., 2011, vol. 6664, pp. 154\u2013168.","journal-title":"Proc. 17th Int. Symp. on Formal Methods. Lect. Notes Compt. Sci."},{"key":"6342_CR12","first-page":"348","volume":"6355","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M., Dafny: an automatic program verifier for functional correctness, Revised Selected Papers of 16th Int. Conf. LPAR-16, Lect. Notes Compt. Sci., 2010, vol. 6355, pp. 348\u2013370.","journal-title":"Revised Selected Papers of 16th Int. Conf. LPAR-16, Lect. Notes Compt. Sci."},{"key":"6342_CR13","first-page":"50","volume-title":"Proc. of 4th Workshop \u201cPSSV: Theory and Applications\u201d, Ekaterinburg","author":"IV Maryasov","year":"2013","unstructured":"Maryasov, I.V., Nepomniaschy, V.A., Promsky, A.V., and Kondratyev, D.A., Automatic C program verification based on mixed axiomatic semantics, Proc. of 4th Workshop \u201cPSSV: Theory and Applications\u201d, Ekaterinburg, 2013, pp. 50\u201359."},{"key":"6342_CR14","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume":"4963","author":"L de Moura","year":"2008","unstructured":"Moura, L. de and Bj\u00f8rner, N., Z3: An efficient SMT solver, Proc. 14th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-2008), Lect. Notes Compt. Sci., 2008, vol. 4963, pp. 337\u2013340.","journal-title":"Proc. 14th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-2008), Lect. Notes Compt. Sci."},{"key":"6342_CR15","doi-asserted-by":"publisher","first-page":"413","DOI":"10.3103\/S014641161107011X","volume":"45","author":"VA Nepomniaschy","year":"2011","unstructured":"Nepomniaschy, V.A., Anureev, I.S., Atuchin, M.M., Maryasov, I.V., Petrov, A.A., and Promsky, A.V., C program verification in SPECTRUM multilanguage system, Autom. Control Compt. Sci., 2011, vol. 45, pp. 413\u2013420.","journal-title":"Autom. Control Compt. Sci."},{"key":"6342_CR16","volume-title":"Preprint Sib. Branch Inst. Inform. System Russ. Acad. Sci.","author":"AV Promsky","year":"2012","unstructured":"Promsky, A.V., A Formal Approach to the Error Localization, Preprint Sib. Branch Inst. Inform. System Russ. Acad. Sci., Novosibirsk, 2012, No. 169."}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411614070141.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411614070141","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411614070141","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411614070141.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T21:58:55Z","timestamp":1773611935000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411614070141"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12]]},"references-count":16,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2014,12]]}},"alternative-id":["6342"],"URL":"https:\/\/doi.org\/10.3103\/s0146411614070141","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,12]]},"assertion":[{"value":"10 November 2013","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 February 2015","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}