{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:59:35Z","timestamp":1740099575909,"version":"3.37.3"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030349677"},{"type":"electronic","value":"9783030349684"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-34968-4_6","type":"book-chapter","created":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T19:14:54Z","timestamp":1574363694000},"page":"101-119","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Evaluation of Program Slicing in Software Verification"],"prefix":"10.1007","author":[{"given":"Marek","family":"Chalupa","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5873-403X","authenticated-orcid":false,"given":"Jan","family":"Strej\u010dek","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,11,22]]},"reference":[{"key":"6_CR1","series-title":"Addison-Wesley Series in Computer Science\/World Student Series Edition","volume-title":"Compilers: Principles, Techniques, and Tools","author":"AV Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley Series in Computer Science\/World Student Series Edition. Addison-Wesley, Boston (1986). \nhttp:\/\/www.worldcat.org\/oclc\/12285707"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-39176-7_7","volume-title":"Model Checking Software","author":"JD Backes","year":"2013","unstructured":"Backes, J.D., Person, S., Rungta, N., Tkachuk, O.: Regression verification using impact summaries. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 99\u2013116. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39176-7_7"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-030-17502-3_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2019","unstructured":"Beyer, D.: Automatic verification of C and Java programs: SV-COMP 2019. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019, Part III. LNCS, vol. 11429, pp. 133\u2013155. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-17502-3_9"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"issue":"1","key":"6_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D Beyer","year":"2019","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. STTT 21(1), 1\u201329 (2019)","journal-title":"STTT"},{"key":"6_CR6","first-page":"1","volume-title":"Advances in Computers","author":"David W. Binkley","year":"1996","unstructured":"Binkley, D.W., Gallagher, K.B.: Program slicing. In: Advances in Computers, vol. 43, pp. 1\u201350 (1996)"},{"key":"6_CR7","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI 2008, pp. 209\u2013224. USENIX Association (2008)"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Carter, M., He, S., Whitaker, J., Rakamaric, Z., Emmi, M.: SMACK software verification toolchain. In: ICSE 2016, pp. 589\u2013592. ACM (2016)","DOI":"10.1145\/2889160.2889163"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/978-3-319-89963-3_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Chalupa","year":"2018","unstructured":"Chalupa, M., Vitovsk\u00e1, M., Strej\u010dek, J.: SYMBIOTIC 5: boosted instrumentation. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 442\u2013446. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-89963-3_29"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Chebaro, O., Kosmatov, N., Giorgetti, A., Julliand, J.: Program slicing enhances a verification technique combining static and dynamic analysis. In: SAC 2012, pp. 1284\u20131291. ACM (2012)","DOI":"10.1145\/2245276.2231980"},{"issue":"1","key":"6_CR11","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/s10515-013-0127-x","volume":"21","author":"O Chebaro","year":"2014","unstructured":"Chebaro, O., et al.: Behind the scenes in SANTE: a combination of static and dynamic analyses. Autom. Softw. Eng. 21(1), 107\u2013143 (2014)","journal-title":"Autom. Softw. Eng."},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/11691372_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MB Dwyer","year":"2006","unstructured":"Dwyer, M.B., Hatcliff, J., Hoosier, M., Ranganath, V.P., Robby, Wallentine, T.: Evaluating the effectiveness of slicing for model reduction of concurrent object-oriented programs. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, pp. 73\u201389. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11691372_5"},{"issue":"3","key":"6_CR13","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1145\/24039.24041","volume":"9","author":"J Ferrante","year":"1987","unstructured":"Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst. 9(3), 319\u2013349 (1987)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"issue":"3","key":"6_CR15","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1002\/swf.41","volume":"2","author":"M Harman","year":"2001","unstructured":"Harman, M., Hierons, R.M.: An overview of program slicing. Softw. Focus 2(3), 85\u201392 (2001)","journal-title":"Softw. Focus"},{"issue":"4","key":"6_CR16","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1023\/A:1026599015809","volume":"13","author":"J Hatcliff","year":"2000","unstructured":"Hatcliff, J., Dwyer, M.B., Zheng, H.: Slicing software for model construction. Higher-Order Symb. Comput. 13(4), 315\u2013353 (2000)","journal-title":"Higher-Order Symb. Comput."},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Hind, M.: Pointer analysis: haven\u2019t we solved this problem yet? In: PASTE 2001, pp. 54\u201361. ACM (2001)","DOI":"10.1145\/379605.379665"},{"issue":"1","key":"6_CR18","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/77606.77608","volume":"12","author":"S Horwitz","year":"1990","unstructured":"Horwitz, S., Reps, T.W., Binkley, D.W.: Interprocedural slicing using dependence graphs. ACM Trans. Program. Lang. Syst. 12(1), 26\u201360 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_CR19","unstructured":"Ivancic, F., et al.: Model checking C programs using F-SOFT. In: ICCD 2005, pp. 297\u2013308. IEEE Computer Society (2005)"},{"key":"6_CR20","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. 3576, pp. 301\u2013306. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11513988_31"},{"issue":"3","key":"6_CR21","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1016\/j.tcs.2008.03.013","volume":"404","author":"F Ivancic","year":"2008","unstructured":"Ivancic, F., Yang, Z., Ganai, M.K., Gupta, A., Ashar, P.: Efficient SAT-based bounded model checking for software verification. Theor. Comput. Sci. 404(3), 256\u2013274 (2008)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-31424-7_32","volume-title":"Computer Aided Verification","author":"A Lal","year":"2012","unstructured":"Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 427\u2013443. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-31424-7_32"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-319-03077-7_4","volume-title":"Hardware and Software: Verification and Testing","author":"T Lange","year":"2013","unstructured":"Lange, T., Neuh\u00e4u\u00dfer, M.R., Noll, T.: Speeding up the safety verification of programmable logic controller code. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 44\u201360. Springer, Cham (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-319-03077-7_4"},{"key":"6_CR24","unstructured":"Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis & transformation. In: CGO 2004, pp. 75\u201388. IEEE Computer Society (2004)"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-030-17502-3_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Lauko","year":"2019","unstructured":"Lauko, H., \u0160till, V., Ro\u010dkai, P., Barnat, J.: Extending DIVINE with symbolic verification using SMT. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 204\u2013208. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-17502-3_14"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/11813040_27","volume-title":"FM 2006: Formal Methods","author":"X Li","year":"2006","unstructured":"Li, X., Hoover, H.J., Rudnicki, P.: Towards automatic exception safety verification. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 396\u2013411. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11813040_27"},{"key":"6_CR27","unstructured":"Lucia, A.D.: Program slicing: methods and applications. In: SCAM 2001, pp. 144\u2013151. IEEE Computer Society (2001)"},{"issue":"2","key":"6_CR28","first-page":"253","volume":"30","author":"DP Mohapatra","year":"2006","unstructured":"Mohapatra, D.P., Mall, R., Kumar, R.: An overview of slicing techniques for object-oriented programs. Informatica (Slovenia) 30(2), 253\u2013277 (2006)","journal-title":"Informatica (Slovenia)"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-31987-0_7","volume-title":"Programming Languages and Systems","author":"VP Ranganath","year":"2005","unstructured":"Ranganath, V.P., Amtoft, T., Banerjee, A., Dwyer, M.B., Hatcliff, J.: A new foundation for control-dependence and slicing for modern program structures. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 77\u201393. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/978-3-540-31987-0_7"},{"key":"6_CR30","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/j.entcs.2009.12.039","volume":"260","author":"H Sabouri","year":"2010","unstructured":"Sabouri, H., Sirjani, M.: Slicing-based reductions for Rebeca. Electr. Notes Theor. Comput. Sci. 260, 209\u2013224 (2010)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"3","key":"6_CR31","first-page":"121","volume":"3","author":"F Tip","year":"1995","unstructured":"Tip, F.: A survey of program slicing techniques. J. Prog. Lang. 3(3), 121\u2013189 (1995)","journal-title":"J. Prog. Lang."},{"key":"6_CR32","doi-asserted-by":"crossref","unstructured":"Trabish, D., Mattavelli, A., Rinetzky, N., Cadar, C.: Chopped symbolic execution. In: Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, 27 May\u201303 June 2018, pp. 350\u2013360. ACM (2018). \nhttps:\/\/doi.org\/10.1145\/3180155.3180251","DOI":"10.1145\/3180155.3180251"},{"issue":"6","key":"6_CR33","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/j.entcs.2005.04.017","volume":"128","author":"S Vasudevan","year":"2005","unstructured":"Vasudevan, S., Emerson, E.A., Abraham, J.A.: Efficient model checking of hardware using conditioned slicing. Electr. Notes Theor. Comput. Sci. 128(6), 279\u2013294 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1","key":"6_CR34","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-006-0022-x","volume":"9","author":"S Vasudevan","year":"2007","unstructured":"Vasudevan, S., Emerson, E.A., Abraham, J.A.: Improved verification of hardware designs through antecedent conditioned slicing. STTT 9(1), 89\u2013101 (2007)","journal-title":"STTT"},{"key":"6_CR35","doi-asserted-by":"crossref","unstructured":"Wang, L., Zhang, Q., Zhao, P.: Automated detection of code vulnerabilities based on program analysis and model checking. In: SCAM 2008, pp. 165\u2013173. IEEE Computer Society (2008)","DOI":"10.1109\/SCAM.2008.24"},{"issue":"4","key":"6_CR36","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1109\/TSE.1984.5010248","volume":"10","author":"M Weiser","year":"1984","unstructured":"Weiser, M.: Program slicing. IEEE Trans. Softw. Eng. 10(4), 352\u2013357 (1984)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"6_CR37","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1050849.1050865","volume":"30","author":"B Xu","year":"2005","unstructured":"Xu, B., Qian, J., Zhang, X., Wu, Z., Chen, L.: A brief survey of program slicing. ACM SIGSOFT Softw. Eng. Notes 30(2), 1\u201336 (2005)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-34968-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T19:17:30Z","timestamp":1574363850000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-34968-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030349677","9783030349684"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-34968-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"22 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bergen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Norway","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/ifm2019.hvl.no\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}