{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T23:49:53Z","timestamp":1725752993628},"publisher-location":"Berlin, Heidelberg","reference-count":25,"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_5","type":"book-chapter","created":{"date-parts":[[2013,10,21]],"date-time":"2013-10-21T01:11:19Z","timestamp":1382317879000},"page":"53-69","source":"Crossref","is-referenced-by-count":1,"title":["A Proof Slicing Framework for Program Verification"],"prefix":"10.1007","author":[{"given":"Ton Chanh","family":"Le","sequence":"first","affiliation":[]},{"given":"Cristian","family":"Gherghina","sequence":"additional","affiliation":[]},{"given":"Razvan","family":"Voicu","sequence":"additional","affiliation":[]},{"given":"Wei-Ngan","family":"Chin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/j.artint.2004.11.004","volume":"162","author":"E. Amir","year":"2005","unstructured":"Amir, E., McIlraith, S.: Partition-based logical reasoning for first-order and propositional theories. Artificial Intelligence\u00a0162, 49\u201388 (2005)","journal-title":"Artificial Intelligence"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Biere, A., Sinz, C.: Decomposing SAT problems into connected components. JSAT (2006)","DOI":"10.3233\/SAT190022"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Buss, S.R.: An introduction to proof theory. In: Handbook of Proof Theory (1998)","DOI":"10.1016\/S0049-237X(98)80016-5"},{"key":"5_CR4","unstructured":"de Moura, L., Bj\u00f8rner, N.: Relevancy propagation. Technical report, MSR (2007)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Do, H., Elbaum, S.G., Rothermel, G.: Supporting controlled experimentation with testing techniques: An infrastructure and its potential impact. In: ESE, vol.\u00a010 (2005)","DOI":"10.1007\/s10664-005-3861-2"},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/261320.261324","volume":"31","author":"A. Dolzmann","year":"1997","unstructured":"Dolzmann, A., Sturm, T.: Redlog: computer algebra meets computer logic. SIGSAM Bulletin\u00a031, 2\u20139 (1997)","journal-title":"SIGSAM Bulletin"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Fietzke, A., Weidenbach, C.: Labelled splitting. Annals of MAI\u00a055 (2009)","DOI":"10.1007\/s10472-009-9150-9"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL (2004)","DOI":"10.1145\/964001.964021"},{"key":"5_CR10","unstructured":"Huang, H., Tsai, W.-T., Paul, R.A.: Proof slicing with application to model checking web services. In: ISORC, pp. 292\u2013299 (2005)"},{"key":"5_CR11","unstructured":"Klarlund, N., Moller, A.: MONA Version 1.4 - User Manual. BRICS Notes Series (2001)"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Lang, J., Liberatore, P., Marquis, P.: Propositional independence: formula-variable independence and forgetting. Journal of Artificial Intelligence Research\u00a018 (2003)","DOI":"10.1613\/jair.1113"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Le, T.C., Gherghina, C., Voicu, R., Chin, W.N.: A Proof Slicing Framework for Program Verification (2013), http:\/\/www.comp.nus.edu.sg\/~chanhle\/icfem13-long.pdf","DOI":"10.1007\/978-3-642-41202-8_5"},{"key":"5_CR14","unstructured":"Leino, K.R.M., Moskal, M., Schulte, W.: Verification condition splitting (2008)"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-24730-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2004","unstructured":"McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 16\u201330. Springer, Heidelberg (2004)"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. Journal of Applied Logic, 41\u201357 (2009)","DOI":"10.1016\/j.jal.2007.07.004"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Navarro P\u00e9rez, J.A., Rybalchenko, A.: Separation logic + superposition calculus = heap theorem prover. In: PLDI, pp. 556\u2013566 (2011)","DOI":"10.1145\/1993316.1993563"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Nguyen, H.H., David, C., Qin, S.C., Chin, W.N.: Automated Verification of Shape And Size Properties via Separation Logic. In: VMCAI, pp. 251\u2013266 (2007)","DOI":"10.1007\/978-3-540-69738-1_18"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P.W. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J., Yang, H.: Local Reasoning about Programs that Alter Data Structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol.\u00a02142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-61511-3_126","volume-title":"Automated Deduction - Cade-13","author":"T.J. Park","year":"1996","unstructured":"Park, T.J., Gelder, A.V.: Partitioning methods for satisfiability testing on large formulas. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 748\u2013762. Springer, Heidelberg (1996)"},{"key":"5_CR21","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":"5_CR22","unstructured":"Hong, H.S., Lee, I., Sokolsky, O.: Abstract slicing: A new approach to program slicing based on abstract interpretation and model checking. In: SCAM (2005)"},{"key":"5_CR23","unstructured":"S\u00f8rensen, U.: Slicing for Uppaal. Technical report, AALBORG University (2008)"},{"key":"5_CR24","unstructured":"Frama-C Software\u00a0Analyser System (2012), http:\/\/frama-c.com"},{"key":"5_CR25","unstructured":"Torres-Jimenez, J., Vega-Garcia, L., Coutino-Gomez, C.A., Cartujano-Escobar, F.J.: SSTP: An approach to Solve SAT instances Through Partition. In: WSEAS (2004)"}],"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_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,6]],"date-time":"2020-08-06T03:09:49Z","timestamp":1596683389000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41202-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642412011","9783642412028"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41202-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}