{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:49:45Z","timestamp":1773654585419,"version":"3.50.1"},"reference-count":10,"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\/s014641161107011x","type":"journal-article","created":{"date-parts":[[2012,1,5]],"date-time":"2012-01-05T17:57:59Z","timestamp":1325786279000},"page":"413-420","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["C program verification in SPECTRUM multilanguage system"],"prefix":"10.3103","volume":"45","author":[{"given":"V. A.","family":"Nepomniaschy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"I. S.","family":"Anureev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M. M.","family":"Atuchin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"I. V.","family":"Maryasov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. A.","family":"Petrov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. V.","family":"Promsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1627","published-online":{"date-parts":[[2012,1,6]]},"reference":[{"issue":"3","key":"6168_CR1","first-page":"5","volume":"17","author":"I.S. Anureev","year":"2010","unstructured":"Anureev, I.S., Maryasov, I.V., and Nepomniaschy, V.A., C-Program Verification Based on the Mixed Axiomatic Semantics, Modelir. Analiz Inform. Sistem, 2010, vol. 17, no. 3, pp. 5\u201328.","journal-title":"Modelir. Analiz Inform. Sistem"},{"issue":"6","key":"6168_CR2","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 Promskii, 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":"6168_CR3","volume-title":"Sistemnaya informatika: Sb. nauch. tr","author":"V.A. Nepomniaschy","year":"2004","unstructured":"Nepomniaschy, V.A., Anureev, I.S., Mikhailov, I.N., and Promsky, A.V., Verification-Oriented C-Light Language, in Sistemnaya informatika: Sb. nauch. tr (System Informatics. Collection of Scientific Papers), Novosibirsk: Sib. Otd. Ross. Akad. Nauk, 2004, no. 9."},{"issue":"4","key":"6168_CR4","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1134\/S0361768806040025","volume":"32","author":"V.A. Nepomniaschy","year":"2006","unstructured":"Nepomniaschy, V.A., Anureev, I.S., Promsky, A.V., and Dubranovsky, I.V., Towards Verification of C# Programs: A Three-Level Approach, Program. Comput. Software, 2006, vol. 32, no. 4, pp. 190\u2013202].","journal-title":"Program. Comput. Software"},{"key":"6168_CR5","first-page":"1","volume":"28","author":"I.S. Anureev","year":"2008","unstructured":"Anureev, I.S., A Three-Stage Method of C Program Verification, Joint NCC&IIS Bulletin, Series Computer Science, 2008, vol. 28, pp. 1\u201329.","journal-title":"Joint NCC&IIS Bulletin, Series Computer Science"},{"key":"6168_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-87873-5_1","volume":"5295","author":"E. Alkassar","year":"2008","unstructured":"Alkassar, E., Hillebrand, M.A., Leinenbach, D., Schirmer, N.W., and Starostin, A., The Verisoft Approach to System Verification, Proc. Conf. on Verified Software: Theories, Tools and Experiments (VSTTE), 2008, vol. 5295, pp. 1\u201329.","journal-title":"Proc. Conf. on Verified Software: Theories, Tools and Experiments (VSTTE)"},{"key":"6168_CR7","first-page":"23","volume":"5674","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen T., Schulte W., and Tobies, S., VCC: A Practical System for Verifying Concurrent C, Proc. TPHOLs 2009, Lect. Notes Comput. Sci., 2009, vol. 5674, pp. 23\u201342.","journal-title":"Proc. TPHOLs 2009"},{"key":"6168_CR8","doi-asserted-by":"crossref","unstructured":"Filli\u00e1tre, J.C. and March\u00e9, C., Multi-Prover Verification of C Programs, Proc. ICFEM, 2004, pp. 15\u201329.","DOI":"10.1007\/978-3-540-30482-1_10"},{"key":"6168_CR9","first-page":"202","volume":"2852","author":"B. Jacobs","year":"2003","unstructured":"Jacobs, B. and Kiniry, J.L., and Warmer, M., Java Program Verification Challenges, Proc. FMCO 2002, Lect. Notes Comput. Sci., 2003, vol. 2852, pp. 202\u2013219.","journal-title":"Proc. FMCO 2002"},{"key":"6168_CR10","first-page":"53","volume-title":"Proc. International Workshop on Program Understanding","author":"A.V. Promsky","year":"2009","unstructured":"Promsky, A.V., Towards C-Light Program Verification: Overcoming the Obstacles, Proc. International Workshop on Program Understanding, Altai Mountains, Russia, 2009, pp. 53\u201363."}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S014641161107011X.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S014641161107011X","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.3103\/S014641161107011X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S014641161107011X.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T21:58:50Z","timestamp":1773611930000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S014641161107011X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12]]},"references-count":10,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2011,12]]}},"alternative-id":["6168"],"URL":"https:\/\/doi.org\/10.3103\/s014641161107011x","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":"18 October 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"}}]}}