{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T04:23:43Z","timestamp":1775017423636,"version":"3.50.1"},"reference-count":15,"publisher":"Pleiades Publishing Ltd","issue":"8","license":[{"start":{"date-parts":[[2020,12,1]],"date-time":"2020-12-01T00:00:00Z","timestamp":1606780800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2020,12,1]],"date-time":"2020-12-01T00:00:00Z","timestamp":1606780800000},"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":["Program Comput Soft"],"published-print":{"date-parts":[[2020,12]]},"DOI":"10.1134\/s0361768820080046","type":"journal-article","created":{"date-parts":[[2020,12,22]],"date-time":"2020-12-22T07:03:01Z","timestamp":1608620581000},"page":"731-736","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Formal Model for Detecting Bugs by Symbolic Execution of Programs"],"prefix":"10.1134","volume":"46","author":[{"given":"A. Yu.","family":"Gerasimov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D. O.","family":"Kuts","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. A.","family":"Novikov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"137","published-online":{"date-parts":[[2020,12,22]]},"reference":[{"key":"3562_CR1","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1145\/96267.96279","volume":"33","author":"B.P. Miller","year":"2009","unstructured":"Miller, B.P., Fredriksen, L., and So, B., An empirical study of the reliability of UNIX utilities, Comm. ACM, 2009, vol. 33, no. 12, pp. 32\u201344.","journal-title":"Comm. ACM"},{"key":"3562_CR2","unstructured":"Zalewski, M., Symbolic execution in vuln research. https:\/\/lcamtuf.blogspot.com\/2015\/02\/symbolic-execution-in-vuln-research.html"},{"key":"3562_CR3","doi-asserted-by":"crossref","unstructured":"Boyer, R.S., Elspas, B., and Levitt, K.N., SELECT \u2013 a formal system for testing and debugging programs by symbolic execution, Proc. of the International Conference on Reliable software, 1975, pp. 234\u2013245.","DOI":"10.1145\/800027.808445"},{"key":"3562_CR4","first-page":"159","volume":"28","author":"A. Yu. Gerasimov","year":"2016","unstructured":"Gerasimov, A. Yu. and Kruglov, L.V., Input data generation for reaching specific function in program by iterative dynamic analysis method, Trudy ISP RAN, 2016, vol. 28, no. 5, pp. 159\u2013174.","journal-title":"Trudy ISP RAN"},{"key":"3562_CR5","first-page":"111","volume":"29","author":"A. Yu. Gerasimov","year":"2017","unstructured":"Gerasimov, A. Yu. Kruglov, L.V., Ermakov, M.K., and Vartanov, S.P., An approach to determining reachability of program flaws detected by static analysis using dynamic symbolic execution of programs, Trudy ISP RAN, 2017, vol. 29, no. 5, pp. 111\u2013134.","journal-title":"Trudy ISP RAN"},{"key":"3562_CR6","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/2093548.2093564","volume":"55","author":"P. Godefroid","year":"2012","unstructured":"Godefroid, P., Levin, M.Y., and Molnar, D., SAGE: Whitebox fuzzing for security testing, Comm. ACM, 2012, vol. 55, no. 3, pp. 40\u201344.","journal-title":"Comm. ACM"},{"key":"3562_CR7","unstructured":"CWE-476: NULL Pointer Dereference. https:\/\/cwe.mitre.org\/data\/definitions\/476.html"},{"key":"3562_CR8","unstructured":"CWE-121: Stack-based Buffer Overflow. https:\/\/cwe.mitre.org\/data\/definitions\/121.html"},{"key":"3562_CR9","unstructured":"CWE-122: Heap-based Buffer Overflow. https:\/\/cwe.mitre.org\/data\/definitions\/122.html"},{"key":"3562_CR10","unstructured":"CWE-123: Write-what-where Condition. https:\/\/cwe.mitre.org\/data\/definitions\/123.html"},{"key":"3562_CR11","unstructured":"CWE-125: Out-of-bounds Read. https:\/\/cwe.mitre.org\/data\/definitions\/125.html"},{"key":"3562_CR12","unstructured":"CWE-787: Out-of-bounds Write. https:\/\/cwe.mitre.org\/data\/definitions\/787.html"},{"key":"3562_CR13","doi-asserted-by":"crossref","unstructured":"Gerasimov, A., Vartanov, S., Ermakov, M., Kruglov, L., Kutz, D., Novikov, A., and Asryan, S., Anxiety: A dynamic symbolic execution framework, Proc. of the 2017 Ivannikov ISP RAS Open Conference, 2017, pp. 16\u201321.","DOI":"10.1109\/ISPRAS.2017.00010"},{"key":"3562_CR14","first-page":"151","volume":"29","author":"A.N. Fedotov","year":"2017","unstructured":"Fedotov, A.N., Kaushan, V.V., Gaissaryan, S.S., and Kurmangaleev Sh.F., Building security predicates for some types of vulnerabilities, Trudy ISP RAN, 2017, vol. 29, no. 6, pp. 151\u2013162.","journal-title":"Trudy ISP RAN"},{"key":"3562_CR15","doi-asserted-by":"crossref","unstructured":"Bruening, D, Garnett, T., and Amarasinghe, S., An infrastructure for adaptive dynamic optimization, Proc. of the International Symposium on Code Generation and Optimization, 2003, pp. 265\u2013275.","DOI":"10.1109\/CGO.2003.1191551"}],"container-title":["Programming and Computer Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768820080046.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1134\/S0361768820080046","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768820080046.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T02:45:05Z","timestamp":1775011505000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1134\/S0361768820080046"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,12]]},"references-count":15,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["3562"],"URL":"https:\/\/doi.org\/10.1134\/s0361768820080046","relation":{},"ISSN":["0361-7688","1608-3261"],"issn-type":[{"value":"0361-7688","type":"print"},{"value":"1608-3261","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,12]]},"assertion":[{"value":"12 February 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 March 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 March 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 December 2020","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}