乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T10:38:25Z","timestamp":1725791905087},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319064093"},{"type":"electronic","value":"9783319064109"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06410-9_36","type":"book-chapter","created":{"date-parts":[[2014,4,18]],"date-time":"2014-04-18T21:03:01Z","timestamp":1397854981000},"page":"531-546","source":"Crossref","is-referenced-by-count":4,"title":["Efficient Tight Field Bounds Computation Based on Shape Predicates"],"prefix":"10.1007","author":[{"given":"Pablo","family":"Ponzio","sequence":"first","affiliation":[]},{"given":"Nicol\u00e1s","family":"Rosner","sequence":"additional","affiliation":[]},{"given":"Nazareno","family":"Aguirre","sequence":"additional","affiliation":[]},{"given":"Marcelo","family":"Frias","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"36_CR1","doi-asserted-by":"crossref","unstructured":"Abad, P., Aguirre, N., Bengolea, V., Ciolek, D., Frias, M., Galeotti, J., Maibaum, T., Moscato, M., Rosner, N., Vissani, I.: Improving Test Generation under Rich Contracts by Tight Bounds and Incremental SAT Solving. In: ICST 2013 (2013)","DOI":"10.1109\/ICST.2013.46"},{"key":"36_CR2","doi-asserted-by":"crossref","unstructured":"Belt, J., Robby, Deng, X.: Sireum\/Topi LDP: A Lightweight Semi-Decision Procedure for Optimizing Symbolic Execution-based Analyses. In: FSE 2009 (2009)","DOI":"10.1145\/1595696.1595762"},{"key":"36_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-22110-1_15","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2011","unstructured":"Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: Memory safety for systems-level code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 178\u2013183. Springer, Heidelberg (2011)"},{"key":"36_CR4","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. In: ISSTA 2002, pp. 123\u2013133 (2002)","DOI":"10.1145\/566171.566191"},{"key":"36_CR5","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL 2009 (2009)","DOI":"10.1145\/1594834.1480917"},{"key":"36_CR6","doi-asserted-by":"crossref","unstructured":"Dennis, G., Chang, F., Jackson, D.: Verification of Code with SAT. In: ISSTA 2006 (2006)","DOI":"10.1145\/1146238.1146251"},{"key":"36_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-642-22110-1_23","volume-title":"Computer Aided Verification","author":"W.-N. Chin","year":"2011","unstructured":"Chin, W.-N., Gherghina, C., Voicu, R., Le, Q.L., Craciun, F., Qin, S.: A specialization calculus for pruning disjunctive predicates to support verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 293\u2013309. Springer, Heidelberg (2011)"},{"key":"36_CR8","doi-asserted-by":"crossref","unstructured":"Frias, M., Galeotti, J., L\u00f3pez Pombo, C., Aguirre, N.: DynAlloy: Upgrading Alloy with Actions. In: Proc. of ICSE 2005 (2005)","DOI":"10.1145\/1062455.1062535"},{"key":"36_CR9","doi-asserted-by":"crossref","unstructured":"Galeotti, J.P., Rosner, N., Lopez Pombo, C., Frias, M.: Analysis of Invariants for Efficient Bounded Verification. In: ISSTA 2010 (2010)","DOI":"10.1145\/1831708.1831712"},{"key":"36_CR10","doi-asserted-by":"crossref","unstructured":"Galeotti, J.P., Rosner, N., Lopez Pombo, C., Frias, M.: TACO: Efficient SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds. IEEE Trans. Soft. Eng. (2013)","DOI":"10.1109\/TSE.2013.15"},{"key":"36_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-642-38088-4_16","volume-title":"NASA Formal Methods","author":"J. Geldenhuys","year":"2013","unstructured":"Geldenhuys, J., Aguirre, N., Frias, M.F., Visser, W.: Bounded Lazy Initialization. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol.\u00a07871, pp. 229\u2013243. Springer, Heidelberg (2013)"},{"key":"36_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-46017-9_5","volume-title":"Model Checking Software","author":"R. Iosif","year":"2002","unstructured":"Iosif, R.: Symmetry Reduction Criteria for Software Model Checking. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 22\u201341. Springer, Heidelberg (2002)"},{"key":"36_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/11513988_31","volume-title":"Computer Aided Verification","author":"F. Ivan\u010di\u0107","year":"2005","unstructured":"Ivan\u010di\u0107, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-Soft: Software Verification Platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 301\u2013306. Springer, Heidelberg (2005)"},{"key":"36_CR14","unstructured":"Jackson, D.: Software Abstractions. MIT Press (2006)"},{"key":"36_CR15","doi-asserted-by":"crossref","unstructured":"Magill, S., Tsai, M.H., Lee, P., Tsay, Y.K.: Automatic numeric abstractions for heap-manipulating programs. In: POPL 2010 (2010)","DOI":"10.1145\/1706299.1706326"},{"key":"36_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-540-69738-1_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H.H. Nguyen","year":"2007","unstructured":"Nguyen, H.H., David, C., Qin, S., Chin, W.-N.: Automated Verification of Shape and Size Properties via Separation Logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 251\u2013266. Springer, Heidelberg (2007)"},{"key":"36_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-70545-1_34","volume-title":"Computer Aided Verification","author":"H.H. Nguyen","year":"2008","unstructured":"Nguyen, H.H., Chin, W.-N.: Enhancing program verification with lemmas. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 355\u2013369. Springer, Heidelberg (2008)"},{"key":"36_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/978-3-642-24690-6_11","volume-title":"Software Engineering and Formal Methods","author":"B.C. Parrino","year":"2011","unstructured":"Parrino, B.C., Galeotti, J.P., Garbervetsky, D., Frias, M.F.: A Dataflow Analysis to Improve SAT-Based Bounded Program Verification. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol.\u00a07041, pp. 138\u2013154. Springer, Heidelberg (2011)"},{"key":"36_CR19","unstructured":"Reynolds, J.: Separation Logic: A Logic for Shared Mutable Data Structures. In: Proceedings of LICS 2002 (2002)"},{"key":"36_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: A Relational Model Finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 632\u2013647. Springer, Heidelberg (2007)"},{"key":"36_CR21","doi-asserted-by":"crossref","unstructured":"Visser, W., Pasareanu, C.S., Pelanek, R.: Test Input Generation for Java Containers using State Matching. In: ISSTA 2006 (2006)","DOI":"10.1145\/1146238.1146243"},{"key":"36_CR22","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Saturn: A scalable framework for error detection using Boolean satisfiability. ACM TOPLAS\u00a029(3) (2007)","DOI":"10.1145\/1232420.1232423"}],"container-title":["Lecture Notes in Computer Science","FM 2014: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06410-9_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T16:45:16Z","timestamp":1558889116000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06410-9_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319064093","9783319064109"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06410-9_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}