{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:50:13Z","timestamp":1773654613959,"version":"3.50.1"},"reference-count":19,"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\/s0146411614070025","type":"journal-article","created":{"date-parts":[[2015,1,30]],"date-time":"2015-01-30T19:16:45Z","timestamp":1422645405000},"page":"389-397","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Software defect detection by combining bounded model checking and approximations of functions"],"prefix":"10.3103","volume":"48","author":[{"given":"M. Kh.","family":"Akhin","sequence":"first","affiliation":[]},{"given":"M. A.","family":"Belyaev","sequence":"additional","affiliation":[]},{"given":"V. M.","family":"Itsykson","sequence":"additional","affiliation":[]}],"member":"1627","published-online":{"date-parts":[[2015,2,1]]},"reference":[{"key":"6340_CR1","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Proc. Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201904)","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., and Lerda, F.A., Tool for checking ANSI-C programs, Proc. Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201904), 2004, pp. 168\u2013176."},{"key":"6340_CR2","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10009-008-0091-0","volume":"11","author":"A Armando","year":"2009","unstructured":"Armando, A., Mantovani, J., and Platania, L., Bounded model checking of software using SMT solvers instead of SAT solvers, Int. J. Soft. Tools Technol. Transf., 2009, vol. 11, pp. 69\u201383.","journal-title":"Int. J. Soft. Tools Technol. Transf."},{"key":"6340_CR3","first-page":"137","volume-title":"Proc. ASE","author":"L Cordeiro","year":"2009","unstructured":"Cordeiro, L., Fischer, B., and Marques-Silva, J., SMT-based bounded model checking for embedded ANSI-C software, Proc. ASE, 2009, pp. 137\u2013148."},{"key":"6340_CR4","first-page":"146","volume":"7152","author":"F Merz","year":"2012","unstructured":"Merz, F., Falke, S., and Sinz, C., The low-level bounded model checker: Bounded model checking of C and C++ programs using a compiler IR, Compt. Sci., 2012, vol. 7152, pp. 146\u2013161.","journal-title":"Compt. Sci."},{"issue":"101","key":"6340_CR5","first-page":"63","volume":"3","author":"VM Itsykson","year":"2010","unstructured":"Itsykson, V.M., and Glukhikh, M.I., Language of specifications of program component behavior, Nauchno-tehnicheskie vedomosti St. Pb. Gos. Politekh. Univ. Informatika. Telekommunikacii. Upravlenie, 2010, vol. 3, no. 101, pp. 63\u201370.","journal-title":"Nauchno-tehnicheskie vedomosti St. Pb. Gos. Politekh. Univ. Informatika. Telekommunikacii. Upravlenie"},{"key":"6340_CR6","first-page":"8","volume-title":"Proc. CEE-SECR-11; Program. Inzhener.","author":"VM Itsykson","year":"2012","unstructured":"Itsykson, V.M. and Zozulya, A.V., Automated program transformation for migration to new libraries, Proc. CEE-SECR-11; Program. Inzhener., 2012, no. 6, pp. 8\u201314."},{"key":"6340_CR7","volume-title":"ACSL: ANSI\/ISO C Specification Language. Preliminary Design","author":"P Baudin","year":"2008","unstructured":"Baudin, P., Filliatre, J.C., Hubert, T., March\u00e9, C., Monate, B., Moy, Y., and Prevosto, V., ACSL: ANSI\/ISO C Specification Language. Preliminary Design, Version 1.4, 2008. http:\/\/www.frama-c.cea.fr\/download\/acsl-1.4.pdf"},{"key":"6340_CR8","first-page":"160","volume-title":"Proc. Haifa Verification Conf. (HVC-11)","author":"O Sery","year":"2011","unstructured":"Sery, O., Fedyukovich, G., and Sharygina, N., Interpolation-based function summaries in bounded model checking, Proc. Haifa Verification Conf. (HVC-11), 2011, pp. 160\u2013175."},{"key":"6340_CR9","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Proc. 5th Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems, (TACAS\u201999)","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E. M., and Zhu, Y., Symbolic model checking without BDDs, Proc. 5th Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems, (TACAS\u201999), 1999, pp. 193\u2013207."},{"key":"6340_CR10","first-page":"825","volume-title":"Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications","author":"C Barrett","year":"2009","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., and Tinelli, C., Satisfiability modulo theories, in Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, 2009, pp. 825\u2013885."},{"key":"6340_CR11","first-page":"75","volume-title":"Proc. Int. Symp. on Code Generation and Optimization (CGO\u201904)","author":"C Lattner","year":"2004","unstructured":"Lattner, C. and Adve, V., Low-level virtual machine (LLVM): A compilation framework for lifelong program analysis and transformation, Proc. Int. Symp. on Code Generation and Optimization (CGO\u201904), 2004, pp. 75\u201386."},{"key":"6340_CR12","first-page":"451","volume":"13","author":"R Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., and Zadeck, F.K., Efficiently computing static single assignment form and the control dependence graph, Association for Computing Machinery: Transactions on Programming Languages and Systems (ACM TOPLAS), 1991, vol. 13, pp. 451\u2013490.","journal-title":"Association for Computing Machinery: Transactions on Programming Languages and Systems (ACM TOPLAS)"},{"key":"6340_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-31980-1_1","volume-title":"Proc. Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems, (TACAS\u201905)","author":"KL McMillan","year":"2005","unstructured":"McMillan, K.L., Applications of Craig interpolants in model checking, Proc. Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems, (TACAS\u201905), 2005, pp. 1\u201312."},{"key":"6340_CR14","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W., Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory, The J. Symbol. Logic, 1957, vol. 22, pp. 269\u2013285.","journal-title":"The J. Symbol. Logic"},{"key":"6340_CR15","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Proc. Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems, (TACAS\u201908)","author":"L de Moura","year":"2008","unstructured":"de Moura, L. and Bj\u00f8rner, N., Z3: An efficient SMT solver, Proc. Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems, (TACAS\u201908), 2008, pp. 337\u2013340."},{"key":"6340_CR16","first-page":"503","volume-title":"CAV\u201905","author":"C Barrett","year":"2005","unstructured":"Barrett, C., de Moura, L., and Stump, A., Satisfiability Modulo Theories Competition (SMT-Comp.), CAV\u201905, 2005, pp. 503\u2013516."},{"key":"6340_CR17","volume-title":"The 2012 SMT Competition","author":"DR Cok","year":"2012","unstructured":"Cok, D.R., Griggio, A., and Bruttomesso, R., The 2012 SMT Competition. 2012. http:\/\/smtcomp.sourceforge.net\/2012\/"},{"key":"6340_CR18","unstructured":"Coverity. Open Source Report 2011. http:\/\/www.coverity.com\/library\/pdf\/coverity-scan-2011-open-sourceintegrity-report.pdf"},{"key":"6340_CR19","volume-title":"NECLA Static Analysis Benchmarks","author":"NEC Laboratories.","year":"2013","unstructured":"NEC Laboratories. NECLA Static Analysis Benchmarks. 2013. http:\/\/www.nec-labs.com\/research\/system\/systems-SAV-website\/benchmarks.php"}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411614070025.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411614070025","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411614070025","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411614070025.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T21:58:37Z","timestamp":1773611917000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411614070025"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12]]},"references-count":19,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2014,12]]}},"alternative-id":["6340"],"URL":"https:\/\/doi.org\/10.3103\/s0146411614070025","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":"15 September 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"}}]}}