{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T23:03:34Z","timestamp":1773615814006,"version":"3.50.1"},"reference-count":14,"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\/s0146411611070133","type":"journal-article","created":{"date-parts":[[2012,1,5]],"date-time":"2012-01-05T17:57:59Z","timestamp":1325786279000},"page":"428-436","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["F@BOOL@: Experiment with a simple verifying compiler based on SAT-solvers"],"prefix":"10.3103","volume":"45","author":[{"given":"N. V.","family":"Shilov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1627","published-online":{"date-parts":[[2012,1,6]]},"reference":[{"key":"6170_CR1","unstructured":"Aho, A.V., Hopcroft, J.E., and Ulman, J.D., The Design and Analysis of Computer Algorithms, Addison-Wesley, 1974."},{"key":"6170_CR2","unstructured":"Bodin, E.V., Kalinina, N.A., and Shilov, N.V., Project of Verifying FVOOL Compiler. Part 1: General Description of FVOOL Project, Its Place in Component Approach to Programming. Mini-NIL Language-Prototype of the Language of Project Virtual Machine, Preprint of Inst. System Inform. of Sib. Branch. Russ. Acad. Sci., 2005, no. 131."},{"key":"6170_CR3","unstructured":"Bodin, E.V., Kalinina, N.A., and Shilov, N.V., Project of Verifying FVOOL Compiler. Part 2: Logic Annotations in Mini-NIL Language, Their Static Semantics and Semantics of Time of Performance, Preprint of Inst. System Inform. of Sib. Branch. Russ. Acad. Sci., 2006, no. 138."},{"key":"6170_CR4","unstructured":"Deikstra, V.E., A Discipline of Programming, Prentice-Hall, 1976."},{"key":"6170_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The Science of Programming","author":"D. Gries","year":"1981","unstructured":"Gries, D., The Science of Programming, New York: Springer, 1981."},{"key":"6170_CR6","first-page":"206","volume-title":"Sistemnaya informatika","author":"N.V. Shilov","year":"2002","unstructured":"Shilov, N.V., Vodin, E.V., and Ii, I., About Program Logics\u2014Simply, in Sistemnaya informatika, (System Informatics), Novosibirsk: Nauka, 2002, no. 8, pp. 206\u2013249."},{"issue":"6","key":"6170_CR7","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1134\/S0361768808060029","volume":"34","author":"N.V. Shilov","year":"2008","unstructured":"Shilov, N.V., Anureev, I.S., and Bodin, E.V., Generation of Correctness Conditions for Imperative Programs, Program. Comput. Software, 2008, vol. 34, no. 6, pp. 307\u2013321.","journal-title":"Program. Comput. Software"},{"key":"6170_CR8","unstructured":"Shilov, N.V., Notes about Three Paradigms of Programming, Kompyut. Instrum. Obrazovan., 2010, no. 2, pp. 24\u201337."},{"key":"6170_CR9","first-page":"1","volume":"28","author":"I.S. Anureev","year":"2008","unstructured":"Anureev, I.S., Bodin, E.V., Gorodnyaya, L.V., Marchuk, A.G., Murzin, F.A., and Shilov, N.V., On the Problem of Computer Language Classification, Joint NCC and IIS Bulletin, Ser. Computer Sci., 2008, vol. 28, pp. 1\u201329.","journal-title":"Joint NCC and IIS Bulletin, Ser. Computer Sci."},{"key":"6170_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24756-2_1","volume":"2999","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook B., Levin V., and Rajamani, S.K., SLAM and Static Driver Verifier: Technology Transfer of Formal Methods Inside Microsoft, Lect. Notes Compt. Sci., 2004, vol. 2999, pp. 1\u201320.","journal-title":"Lect. Notes Compt. Sci."},{"key":"6170_CR11","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., and Majumdar, R., The Software Model Checker Blast: Applications to Software Engineering, Int. J. Software Tools Techn. Transf., 2007, no. 9, pp. 505\u2013525.","DOI":"10.1007\/s10009-007-0044-z"},{"key":"6170_CR12","doi-asserted-by":"crossref","unstructured":"Floyd, R.W., Assigning Meanings to Programs. Proc. Symp. in Applied Mathematics. Mathematical Aspects of Computer Science, 1967, pp. 19\u201332.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"6170_CR13","first-page":"1","volume":"2890","author":"C.A.R. Hoare","year":"2003","unstructured":"Hoare, C.A.R., The Verifying Compiler: A Grand Challenge for Computing Research. Perspectives of Systems Informatics (PSI\u20192003), Lect. Notes Compt. Sci., 2003, vol. 2890, pp. 1\u201312.","journal-title":"The Verifying Compiler: A Grand Challenge for Computing Research. Perspectives of Systems Informatics (PSI\u20192003), Lect. Notes Compt. Sci."},{"key":"6170_CR14","first-page":"121","volume":"29","author":"N.V. Shilov","year":"2009","unstructured":"Shilov, N.V., Bodin, Eu.V, and Shilova, S.O., Fabulous Arrays 1: Operational and Transformational Semantics of Static Arrays in Verification FBOOL Project, Bull. Nov. Comp. Center, Comp. Sci., 2009, vol. 29, pp. 121\u2013140.","journal-title":"Bull. Nov. Comp. Center, Comp. Sci."}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411611070133.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411611070133","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411611070133","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411611070133.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:05:02Z","timestamp":1773612302000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411611070133"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12]]},"references-count":14,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2011,12]]}},"alternative-id":["6170"],"URL":"https:\/\/doi.org\/10.3103\/s0146411611070133","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":"26 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"}}]}}