{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:54:14Z","timestamp":1773615254635,"version":"3.50.1"},"reference-count":12,"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\/s0146411611070121","type":"journal-article","created":{"date-parts":[[2012,1,5]],"date-time":"2012-01-05T17:57:59Z","timestamp":1325786279000},"page":"421-427","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verification and synthesis of addition programs under the rules of correctness of statements"],"prefix":"10.3103","volume":"45","author":[{"given":"V. I.","family":"Shelekhov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1627","published-online":{"date-parts":[[2012,1,6]]},"reference":[{"key":"6169_CR1","unstructured":"Karnaukhov, N.S., Pershin, D.Yu., and Shelekhov, V.I., Yazyk predikatnogo programmirovaniya P (P Language of Predicate Programming), Novosibirsk, 2010."},{"key":"6169_CR2","unstructured":"Shelekhov, V., The Language of Calculus of Computable Predicates as a Minimal Kernel for Functional Languages, Bulletin of the Novosibirsk Computing Center. Series: Computer Science. IIS Special Number 2009, 2009, no. 29, pp. 107\u2013117."},{"key":"6169_CR3","unstructured":"Shelekhov, V.I., Model\u2019 korrektnosti programm na yazyke ischisleniya vychislimykh predikatov (Model of Program Correctness on the Language of Calculus of Computable Predicates), Novosibirsk, 2007."},{"key":"6169_CR4","volume-title":"Advanced Computer Arithmetic Design","author":"M.J. Flynn","year":"2001","unstructured":"Flynn, M.J. and Oberman, S.F., Advanced Computer Arithmetic Design, New York: Wiley, 2001. http:\/\/en.wikipedia.org\/wiki\/adder-(electronics)"},{"key":"6169_CR5","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume":"607","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., and Shankar, N., PVS: A Prototype Verification System, Lect. Notes Compt. Sci., 1992, vol. 607, pp. 748\u2013752. http:\/\/pvs.csl.sri.com\/","journal-title":"Lect. Notes Compt. Sci."},{"key":"6169_CR6","unstructured":"Sorensen, M.H. and Urzyczyn, P., Lectures on the Carry-Howard Isomorphism, in Logic and the Foundations of Mathematics, 2006, vol. 149."},{"key":"6169_CR7","unstructured":"Hehner, E.C.R., A Practical Theory of Programming, University of Toronto, 2004. http:\/\/www.cs.toronto.edu\/henner\/aptop\/"},{"issue":"9","key":"6169_CR8","doi-asserted-by":"publisher","first-page":"1110","DOI":"10.1109\/12.2261","volume":"37","author":"R.W. Doran","year":"1988","unstructured":"Doran, R.W., Variants of an Improved Carry Look-Ahead Adder, IEEE Trans. Compt., 1988, vol. 37, no. 9, pp. 1110\u20131113.","journal-title":"IEEE Trans. Compt."},{"key":"6169_CR9","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-540-25951-0_2","volume":"3049","author":"D. Basin","year":"2004","unstructured":"Basin, D., DeVille, Y., Flener, P., Hamfelt, A., and Nilsson, J., Synthesis of Programs in Computational Logic, Lect. Notes Compt. Sci., 2004, vol. 3049, pp. 30\u201365.","journal-title":"Lect. Notes Compt. Sci."},{"key":"6169_CR10","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., and Foster, J., From Program Verification to Program Synthesis, Proc. Symp. on Principles of Programming Languages (POPL), 2010, pp. 313\u2013326.","DOI":"10.1145\/1706299.1706337"},{"key":"6169_CR11","unstructured":"Shelekhov, V.I., Verification and Synthesis of the Effective Programs of Standard floor, isqrt and ilog2 Functions in Predicate Programming Technology, Tr. 12-i Mezhd. Konf. \u201cProblemy Upravleniya i Modelirovaniya V Slozhnykh Sistemakh\u201d, (Proc. 12th Int. Conf. \u201cManagement and Modeling Problems in Complicated Systems\u201d), Samarskii Nauchnyi Tsentr Ross. Akad. Nauk, 2010, pp. 622\u2013630."},{"issue":"2","key":"6169_CR12","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1023\/A:1008610818519","volume":"13","author":"D. Kapur","year":"1998","unstructured":"Kapur, D. and Subramaniam, M., Mechanical Verification of Adder Circuits Using Rewrite Rule Laboratory, Formal Methods in System Design, 1998, vol. 13, no. 2, pp. 127\u2013158.","journal-title":"Formal Methods in System Design"}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411611070121.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411611070121","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411611070121","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411611070121.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T21:57:27Z","timestamp":1773611847000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411611070121"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12]]},"references-count":12,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2011,12]]}},"alternative-id":["6169"],"URL":"https:\/\/doi.org\/10.3103\/s0146411611070121","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"}}]}}