乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T15:40:24Z","timestamp":1649173224421},"reference-count":27,"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":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,12,1]],"date-time":"2020-12-01T00:00:00Z","timestamp":1606780800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Program Comput Soft"],"published-print":{"date-parts":[[2020,12]]},"DOI":"10.1134\/s0361768820080071","type":"journal-article","created":{"date-parts":[[2020,12,22]],"date-time":"2020-12-22T12:03:01Z","timestamp":1608638581000},"page":"747-754","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Predicate Extension of Symbolic Memory Graphs for the Analysis of Memory Safety Correctness"],"prefix":"10.1134","volume":"46","author":[{"given":"A. A.","family":"Vasilyev","sequence":"first","affiliation":[]},{"given":"V. S.","family":"Mutilin","sequence":"additional","affiliation":[]}],"member":"137","published-online":{"date-parts":[[2020,12,22]]},"reference":[{"key":"3564_CR1","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., et al., sel4: Formal verification of an OS kernel, Proc. of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, 2009, pp.\u00a0207\u2013220.","DOI":"10.1145\/1629575.1629596"},{"key":"3564_CR2","doi-asserted-by":"crossref","unstructured":"Stewart, G., Beringer, L., Cuellar, S., and Appel, A.W., Compositional CompCert, Proc. of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005, pp. 275\u2013287.","DOI":"10.1145\/2775051.2676985"},{"key":"3564_CR3","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume":"6806","author":"D. Beyer","year":"2011","unstructured":"Beyer, D. and Keremoglu, M.E., CPAchecker: A tool for configurable software verification, Lect. Notes Comput. Sci., 2011, vol. 6806, pp. 184-190.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3564_CR4","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-642-23702-7_26","volume":"6887","author":"A.F. Donaldson","year":"2011","unstructured":"Donaldson, A.F., Haller, L., Kroening, D., and R\u00fcmmer P., Software verification using k-induction, Lect. Notes Comput. Sci., 2011, vol. 6887, pp. 351\u2013368.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3564_CR5","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume":"1855","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H., Counterexample-guided abstraction refinement, Lect. Notes Comput. Sci., 2000, vol. 1855, pp. 154\u2013169.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3564_CR6","unstructured":"Beyer, D., Keremoglu, M.E., and Wendler, P., Predicate abstraction with adjustable-block encoding, Proc. of the 10th International Conference on Formal Methods in Computer-Aided Design, 2010, pp. 189\u2013197."},{"key":"3564_CR7","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T., and Th\u00e9oduloz, G., Program analysis with dynamic precision adjustment, Proc. of the 23rd IEEE\/ACM International Conference on Automated Software Engineering, 2008, pp. 29\u201338.","DOI":"10.1109\/ASE.2008.13"},{"key":"3564_CR8","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-37057-1_11","volume":"7793","author":"D. Beyer","year":"2013","unstructured":"Beyer, D. and L\u00f6we, S., Explicit-state software model checking based on CEGAR and interpolation, Lecture Notes in Computer Science, 2013, vol. 7793, pp. 146\u2013162.","journal-title":"Lecture Notes in Computer Science"},{"key":"3564_CR9","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume":"1579","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., and Zhu, Y., Symbolic model checking without bdds, Lect. Notes Comput. Sci., 1999, vol. 1579, pp. 193\u2013207.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3564_CR10","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume":"1254","author":"S. Graf","year":"1997","unstructured":"Graf, S. and Saidi, H., Construction of abstract state graphs with PVS, Lect. Notes Comput. Sci., 1997, vol.\u00a01254, pp. 72\u201383.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3564_CR11","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-662-54580-5_22","volume":"10206","author":"P. Andrianov","year":"2017","unstructured":"Andrianov, P., Friedberger, K., Mandrykin, M., Mutilin, V., and Volkov, A., CPA-BAM-BnB: Block-abstraction memoization and region-based memory models for predicate abstractions, Lect. Notes Comput. Sci.,2017, vol. 10206, pp. 355\u2013359.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3564_CR12","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-70545-1_36","volume":"5123","author":"H. Yang","year":"2008","unstructured":"Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., and O\u2019Hearn, P., Scalable shape analysis for systems code, Lect. Notes Comput. Sci., 2008, vol.\u00a05123, pp. 385\u2013398.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3564_CR13","doi-asserted-by":"publisher","first-page":"203216","DOI":"10.15514\/ISPRAS-2017-29(4)-13","volume":"29","author":"A. Volkov","year":"2017","unstructured":"Volkov, A. and Mandrykin, M., Predicate abstractions memory modeling method with separation into disjoint regions, Trudy ISP RAS, 2017, vol. 29, no. 4, pp. 203216. https:\/\/doi.org\/10.15514\/ISPRAS-2017-29(4)-13","journal-title":"Trudy ISP RAS"},{"key":"3564_CR14","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T., Jhala, R., and Majumdar, R., The software model checker BLAST, Int. J. Software Tools Techn. Transfer, 2007, vol. 9, no. 5\u20136, pp. 505\u2013525.","journal-title":"Int. J. Software Tools Techn. Transfer"},{"key":"3564_CR15","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/978-3-642-28756-5_39","volume":"7214","author":"P. Shved","year":"2012","unstructured":"Shved, P., Mandrykin, M., and Mutilin, V., Predicate analysis with BLAST 2.7, Lect. Notes Comput. Sci., 2012, vol. 7214, pp. 525\u2013527.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3564_CR16","unstructured":"Ball, T., Bounimova, E., Kumar, R., and Levin, V., SLAM2: Static driver verification with under 4% false alarms, Proc. of the 10th International Conference on Formal Methods in Computer-Aided Design, 2010, pp.\u00a035\u201342."},{"key":"3564_CR17","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T.W., and Wilhelm, R., Parametric shape analysis via 3-valued logic, ACM Trans. Program. Lang. Syst., 2002, vol. 24, no. 3, pp. 217\u2013298.","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"3564_CR18","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/11817963_48","volume":"4144","author":"D. Beyer","year":"2006","unstructured":"Beyer, D., Henzinger, T.A., and Th\u00e9oduloz, G., Lazy shape analysis, Lect. Notes Comput. Sci., 2006, vol. 4144, pp. 532\u2013546.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3564_CR19","unstructured":"Reynolds, J.C., Separation logic: A logic for shared mutable data structures, Proc. of the 17th Annual IEEE Symposium on Logic in Computer Science, 2002, pp. 55\u201374."},{"key":"3564_CR20","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-22110-1_15","volume":"6806","author":"J. Berdine","year":"2011","unstructured":"Berdine, J., Cook, B., and Ishtiaq, S., Slayer memory safety for systems-level code, Lect. Notes Comput. Sci., 2011, vol. 6806, pp. 178\u2013183.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3564_CR21","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-17164-2_21","volume":"6461","author":"B. Jacobs","year":"2010","unstructured":"Jacobs, B., Smans, J., and Piessens, F., A quick tour of the verifast program verifier, Lect. Notes Comput. Sci., 2010, vol. 6461, pp. 304\u2013311.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3564_CR22","doi-asserted-by":"publisher","first-page":"203","DOI":"10.15514\/ISPRAS-2017-29(4)-13","volume":"29","author":"A. Volkov","year":"2017","unstructured":"Volkov A. and Mandrykin, M., Predicate abstractions memory modeling method with separation into disjoint regions, Trudy ISP RAN, 2017, vol. 29, no. 4, pp. 203\u2013216. https:\/\/doi.org\/10.15514\/ISPRAS-2017-29(4)-13","journal-title":"Trudy ISP RAN"},{"key":"3564_CR23","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-17524-9_1","volume":"9058","author":"C. Calcagno","year":"2015","unstructured":"Calcagno, C., Distefano, D., et al., Moving fast with software verification, Lect. Notes Comput. Sci., 2015, vol. 9058, pp. 3\u201311.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3564_CR24","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-030-17502-3_9","volume":"11429","author":"D. Beyerm","year":"2019","unstructured":"Beyerm D.m Automatic verification of C and Java Programs, SV-COMP 2019, Lect. Notes Comput. Sci., 2019, vol. 11429, pp. 133\u2013155.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3564_CR25","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-642-38856-9_13","volume":"7935","author":"K. Dudka","year":"2013","unstructured":"Dudka, K., Peringer, P., and Vojnar, T., Byte-precise verification of low-level list manipulation, Lect. Notes Comput. Sci., 2013, vol. 7935, pp. 215\u2013237.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3564_CR26","doi-asserted-by":"publisher","first-page":"143","DOI":"10.15514\/ISPRAS-2018-30(6)-8","volume":"30","author":"A.A. Vasilyev","year":"2018","unstructured":"Vasilyev, A.A., Static verification for memory safety of Linux kernel drivers, Trudy ISP RAN, 2018, vol. 30, no.\u00a06, pp. 143\u2013160. https:\/\/doi.org\/10.15514\/ISPRAS-2018-30(6)-8","journal-title":"Trudy ISP RAN"},{"key":"3564_CR27","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-319-74313-4_30","volume":"10742","author":"E. Novikov","year":"2018","unstructured":"Novikov, E. and Zakharov, I., Towards automated static verification of GNU C programs, Lect. Notes Comput. Sci., 2018, vol. 10742, pp. 402\u2013416.","journal-title":"Lect. Notes Comput. Sci."}],"container-title":["Programming and Computer Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768820080071.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1134\/S0361768820080071\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768820080071.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,22]],"date-time":"2020-12-22T12:08:15Z","timestamp":1608638895000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1134\/S0361768820080071"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,12]]},"references-count":27,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["3564"],"URL":"https:\/\/doi.org\/10.1134\/s0361768820080071","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":"2 February 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 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"}}]}}