{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:08Z","timestamp":1751662868474},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642412011"},{"type":"electronic","value":"9783642412028"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41202-8_26","type":"book-chapter","created":{"date-parts":[[2013,10,21]],"date-time":"2013-10-21T01:11:19Z","timestamp":1382317879000},"page":"397-414","source":"Crossref","is-referenced-by-count":3,"title":["Automated Specification Discovery via User-Defined Predicates"],"prefix":"10.1007","author":[{"given":"Guanhua","family":"He","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wei-Ngan","family":"Chin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florin","family":"Craciun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-540-73368-3_51","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Configurable software verification: Concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 504\u2013518. Springer, Heidelberg (2007)"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Dragoi, C., Enea, C., Sighireanu, M.: On inter-procedural analysis of programs with lists and data. In: PLDI (2011)","DOI":"10.1145\/1993498.1993566"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-27940-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Bouajjani","year":"2012","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: Abstract domains for automated reasoning about list-manipulating programs with infinite data. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 1\u201322. Springer, Heidelberg (2012)"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Bozga, M., Iosif, R., Lakhnech, Y.: Storeless semantics and alias logic. In: PEPM (2003)","DOI":"10.1145\/777388.777395"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM\u00a058(6) (2011)","DOI":"10.1145\/2049697.2049700"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Chang, B.Y.E., Rival, X.: Relational inductive shape analysis. In: POPL (2008)","DOI":"10.1145\/1328438.1328469"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Chin, W.N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. of Comp. Prog.\u00a077 (2012)","DOI":"10.1016\/j.scico.2010.07.004"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/11823230_16","volume-title":"Static Analysis","author":"A. Gotsman","year":"2006","unstructured":"Gotsman, A., Berdine, J., Cook, B.: Interprocedural shape analysis with separated heap abstractions. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 240\u2013260. Springer, Heidelberg (2006)"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Lev-Ami, T., Sagiv, M.: A combination framework for tracking partition sizes. In: Shao, Z., Pierce, B.C. (eds.) POPL (2009)","DOI":"10.1145\/1594834.1480912"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Guo, B., Vachharajani, N., August, D.I.: Shape analysis with inductive recursion synthesis. In: PLDI (2007)","DOI":"10.1145\/1250734.1250764"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Hackett, B., Rugina, R.: Region-based shape analysis with tracked locations. In: POPL (2005)","DOI":"10.1145\/1040305.1040331"},{"key":"26_CR13","unstructured":"He, G., Qin, S., Chin, W.N., Craciun, F.: Automated specification discovery in a combined abstract domain - reseach report (2012), \n                    \n                      http:\/\/pls.tees.ac.uk\/~guan\/fullspec\/techreport.pdf"},{"key":"26_CR14","unstructured":"Jonkers, H.: Abstract storage structures. In: Algorithmic Languages (1981)"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Lam, P., Rinard, M.C.: Role analysis. In: POPL (2002)","DOI":"10.1145\/503272.503276"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using smt solvers. In: POPL (2008)","DOI":"10.1145\/1328438.1328461"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-540-70545-1_41","volume-title":"Computer Aided Verification","author":"S. Magill","year":"2008","unstructured":"Magill, S., Tsai, M.-H., Lee, P., Tsay, Y.-K.: Thor: A tool for reasoning about shape and arithmetic. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 428\u2013432. Springer, Heidelberg (2008)"},{"key":"26_CR18","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)","DOI":"10.1145\/1706299.1706326"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"Qin, S., He, G., Luo, C., Chin, W.N., Chen, X.: Loop invariant synthesis in a combined abstract domain. Journal of Symbolic Computation\u00a050 (2013)","DOI":"10.1016\/j.jsc.2012.08.007"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-21437-0_28","volume-title":"FM 2011: Formal Methods","author":"S. Qin","year":"2011","unstructured":"Qin, S., Luo, C., Chin, W.-N., He, G.: Automatically refining partial specifications for program verification. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 369\u2013385. Springer, Heidelberg (2011)"},{"key":"26_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-540-75596-8_18","volume-title":"Automated Technology for Verification and Analysis","author":"Z. Rakamari\u0107","year":"2007","unstructured":"Rakamari\u0107, Z., Bruttomesso, R., Hu, A.J., Cimatti, A.: Verifying heap-manipulating programs in an smt framework. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol.\u00a04762, pp. 237\u2013252. Springer, Heidelberg (2007)"},{"key":"26_CR22","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS (2002)"},{"key":"26_CR23","doi-asserted-by":"crossref","unstructured":"Rival, X., Chang, B.Y.E.: Calling context abstraction with shapes. In: POPL (2011)","DOI":"10.1145\/1926385.1926406"},{"key":"26_CR24","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst.\u00a024(3) (2002)","DOI":"10.1145\/514188.514190"},{"key":"26_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-540-93900-9_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V. Vafeiadis","year":"2009","unstructured":"Vafeiadis, V.: Shape-value abstraction for verifying linearizability. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 335\u2013348. Springer, Heidelberg (2009)"},{"key":"26_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-70545-1_36","volume-title":"Computer Aided Verification","author":"H. Yang","year":"2008","unstructured":"Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 385\u2013398. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41202-8_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,23]],"date-time":"2019-05-23T17:29:10Z","timestamp":1558632550000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41202-8_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642412011","9783642412028"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41202-8_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}