{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T06:16:32Z","timestamp":1784873792824,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642221095","type":"print"},{"value":"9783642221101","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22110-1_23","type":"book-chapter","created":{"date-parts":[[2011,7,4]],"date-time":"2011-07-04T09:08:45Z","timestamp":1309770525000},"page":"293-309","source":"Crossref","is-referenced-by-count":9,"title":["A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification"],"prefix":"10.1007","author":[{"given":"Wei-Ngan","family":"Chin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cristian","family":"Gherghina","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"R\u0103zvan","family":"Voicu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Quang Loc","family":"Le","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Florin","family":"Craciun","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-540-73368-3_22","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2007","unstructured":"Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W., Wies, T., Yang, H.: Shape analysis for composite data structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 178\u2013192. Springer, Heidelberg (2007)"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Chang, B.-Y.E., Rival, X.: Relational inductive shape analysis. In: POPL, pp. 247\u2013260 (2008)","DOI":"10.1145\/1328438.1328469"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Chin, W.N., Gherghina, C., Voicu, R., Le, Q.L., Craciun, F.: A specialization calculus for pruning disjunctive predicates to support verification. Technical report, School of Computing. National University of Singapore (2011), http:\/\/loris-7.ddns.comp.nus.edu.sg\/~project\/hippruning","DOI":"10.1007\/978-3-642-22110-1_23"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"23_CR5","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. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"Guo, B., Vachharajani, N., August, D.I.: Shape analysis with inductive recursion synthesis. In: ACM PLDI, pp. 256\u2013265 (2007)","DOI":"10.1145\/1250734.1250764"},{"key":"23_CR8","volume-title":"Partial Evaluation and Automatic Program Generation","author":"N.D. Jones","year":"1993","unstructured":"Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall, Englewood Cliffs (1993)"},{"key":"23_CR9","unstructured":"Klarlund, N., Moller, A.: MONA Version 1.4 - User Manual. BRICS Notes Series (January 2001)"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-642-11957-6_21","volume-title":"Programming Languages and Systems","author":"V. Laviron","year":"2010","unstructured":"Laviron, V., Chang, B.-Y.E., Rival, X.: Separating shape graphs. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 387\u2013406. Springer, Heidelberg (2010)"},{"issue":"3","key":"23_CR11","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1145\/982158.982159","volume":"26","author":"M. Leuschel","year":"2004","unstructured":"Leuschel, M.: A framework for the integration of partial evaluation and abstract interpretation of logic programs. ACM Trans. Program. Lang. Syst.\u00a026(3), 413\u2013463 (2004)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-71209-1_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Manevich","year":"2007","unstructured":"Manevich, R., Berdine, J., Cook, B., Ramalingam, G., Sagiv, M.: Shape analysis by graph decomposition. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 3\u201318. Springer, Heidelberg (2007)"},{"key":"23_CR13","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":"23_CR14","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.C., 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)"},{"issue":"6","key":"23_CR15","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). J. ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"Podelski, A., Wies, T.: Counterexample-guided focus. In: ACM POPL, pp. 249\u2013260 (2010)","DOI":"10.1145\/1706299.1706330"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"Puebla, G., Hermenegildo, M.: Abstract specialization and its applications. In: ACM SIGPLAN PEPM, pp. 29\u201343 (2003)","DOI":"10.1145\/777388.777393"},{"key":"23_CR18","unstructured":"Puebla, G., Hermenegildo, M., Gallagher, J.P.: An integration of partial evaluation in a generic abstract interpretation framework. In: ACM SIGPLAN PEPM, January 1999, pp. 75\u201384 (1999)"},{"key":"23_CR19","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/135226.135233","volume":"8","author":"W. Pugh","year":"1992","unstructured":"Pugh, W.: The Omega Test: A fast practical integer programming algorithm for dependence analysis. Communications of the ACM\u00a08, 102\u2013114 (1992)","journal-title":"Communications of the ACM"},{"key":"23_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-71316-6_16","volume-title":"Programming Languages and Systems","author":"N. Rinetzky","year":"2007","unstructured":"Rinetzky, N., Poetzsch-Heffter, A., Ramalingam, G., Sagiv, M., Yahav, E.: Modular shape analysis for dynamically encapsulated programs. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 220\u2013236. Springer, Heidelberg (2007)"},{"issue":"3","key":"23_CR21","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst.\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"23_CR22","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods in Computer-Aided Design","author":"J.P. Marques Silva","year":"1996","unstructured":"Marques Silva, J.P., Sakallah, K.A.: GRASP\u2014a new search algorithm for satisfiability. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, Springer, Heidelberg (1996)"},{"key":"23_CR23","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","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22110-1_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T13:41:03Z","timestamp":1560346863000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22110-1_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642221095","9783642221101"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22110-1_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}