{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:46:44Z","timestamp":1773654404235,"version":"3.50.1"},"reference-count":11,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2011,12,1]],"date-time":"2011-12-01T00:00:00Z","timestamp":1322697600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2011,12,1]],"date-time":"2011-12-01T00:00:00Z","timestamp":1322697600000},"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. Conrol Comp. Sci."],"published-print":{"date-parts":[[2011,12]]},"DOI":"10.3103\/s0146411611070029","type":"journal-article","created":{"date-parts":[[2012,1,5]],"date-time":"2012-01-05T17:57:59Z","timestamp":1325786279000},"page":"485-500","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["C-programs verification based on mixed axiomatic semantics"],"prefix":"10.3103","volume":"45","author":[{"given":"I. S.","family":"Anureev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"I. V.","family":"Maryasov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"V. A.","family":"Nepomniaschy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1627","published-online":{"date-parts":[[2012,1,6]]},"reference":[{"key":"6176_CR1","volume-title":"Sistemnaya informatika: sbornik nauchnykh trudov","author":"V.A. Nepomniaschy","year":"2004","unstructured":"Nepomniaschy, V.A., Anureev, I.S., Mikhailov, I.N., and Promsky, A.V., C-Light Language Oriented on Verification, in Sistemnaya informatika: sbornik nauchnykh trudov (Systematic Informatics: Collection of Scientific Papers), Novosibirsk: Sib. Otd. Ross. Akad. Nauk, 2004, no. 9."},{"key":"6176_CR2","unstructured":"Nepomniaschy, V.A., Anureev, I.S., and Promsky, A.V., Towards Verification of C-Programs. C-Light Language and Its Transformational Semantics, Problems in Programming, 2006, nos. 2\u20133, pp. 359\u2013368."},{"issue":"6","key":"6176_CR3","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1023\/A:1021045909505","volume":"28","author":"V.A. Nepomniaschy","year":"2002","unstructured":"Nepomniaschy, V.A., Anureev, I.S., Mikhailov, I.N., and Promsky, A.V., Towards Verification of C Programs. C-Light Language and Its Formal Semantics, Program. Comput. Software, 2002, vol. 28, no. 6, pp. 314\u2013323.","journal-title":"Program. Comput. Software"},{"issue":"6","key":"6176_CR4","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1023\/B:PACS.0000004134.24714.e5","volume":"29","author":"V.A. Nepomniaschy","year":"2003","unstructured":"Nepomniaschy, V.A., Anureev, I.S., Mikhailov, I.N., and Promsky, A.V., Towards Verification of C Programs: Axiomatic Semantics of the C-kernel Language, Program. Comput. Software, 2003, vol. 29, no. 6, pp. 338\u2013350.","journal-title":"Program. Comput. Software"},{"key":"6176_CR5","unstructured":"Nepomniaschy, V.A., Anureev, I.S., Mikhailov, I.N., and Promsky, A.V., Towards Verification of C Programs. Part 1. C-Light Language, Preprint of Inst. of Inform. Systems, Sib. Branch of Russ. Acad. Sci., Novosibirsk, 2001, no. 84, p. 48."},{"key":"6176_CR6","unstructured":"Maryasov, I.V., Towards Verification of C Programs. Mixed Axiomatic Semantics of C-Kernel Language, Preprint of Inst. of Inform. Systems Sib. Branch of Russ. Acad. Sci., Novosibirsk, 2008, no. 150, p. 32."},{"key":"6176_CR7","unstructured":"Maryasov, I.V., Application of Mixed Axiomatic Semantics of C-Kernel Language to Verification of Topological Sorting Program, Preprint of Inst. of Inform. Systems Sib. Branch of Russ. Acad. Sci., Novosibirsk, 2010, no. 155, p. 33."},{"key":"6176_CR8","volume-title":"Prikladnye metody verifikatsii programm","author":"V.A. Nepomniaschy","year":"1988","unstructured":"Nepomniaschy, V.A. and Ryakin, O.M., Prikladnye metody verifikatsii programm (Applied Methods of Program Verification), Moscow: Radio i Svyaz\u2019, 1988."},{"key":"6176_CR9","unstructured":"Programming languages \u2014 C: ISO\/IEC 9899:1999. 1999."},{"key":"6176_CR10","unstructured":"Maryasov, I.V., Towards Automatic Verification of C-Light Programs. Mixed Axiomatic Semantics of C-Kernel Language, Perspectives of Systems Informatics (PSI); (Proc. 7th Int. Conf. on Program Understanding), Novosibirsk, 2009. p. 44\u201352."},{"key":"6176_CR11","unstructured":"Norrish, M., C Formalised in HOL, Thes. doct. phylosophy (computer sci.), Cambridge, 1998."}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411611070029.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411611070029","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411611070029","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411611070029.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T21:58:43Z","timestamp":1773611923000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411611070029"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12]]},"references-count":11,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2011,12]]}},"alternative-id":["6176"],"URL":"https:\/\/doi.org\/10.3103\/s0146411611070029","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,12]]},"assertion":[{"value":"25 May 2010","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 January 2012","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}