{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,6]],"date-time":"2026-07-06T14:27:04Z","timestamp":1783348024407,"version":"3.54.6"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032306920","type":"print"},{"value":"9783032306937","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T00:00:00Z","timestamp":1782950400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T00:00:00Z","timestamp":1782950400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2027]]},"DOI":"10.1007\/978-3-032-30693-7_10","type":"book-chapter","created":{"date-parts":[[2026,7,6]],"date-time":"2026-07-06T14:08:14Z","timestamp":1783346894000},"page":"157-173","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["QCP: A Practical Separation Logic-Based C Program Verification Tool"],"prefix":"10.1007","author":[{"given":"Xiwei","family":"Wu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yueyang","family":"Feng","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xiaoyang","family":"Lu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tianchuan","family":"Lin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kan","family":"Liu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhiyi","family":"Wang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shushu","family":"Wu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lihan","family":"Xie","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chengxi","family":"Yang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hongyi","family":"Zhong","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zihan","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Juanru","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhenjiang","family":"Hu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Qinxiang","family":"Cao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,2]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: modular automatic assertion checking with separation logic. In: Proceedings of the 4th International Conference on Formal Methods for Components and Objects, FMCO\u201905, pp. 115\u2013137. Springer-Verlag, Berlin (2005). https:\/\/doi.org\/10.1007\/11804192_6","DOI":"10.1007\/11804192_6"},{"key":"10_CR2","doi-asserted-by":"publisher","unstructured":"Beringer, L.: Verified software units. In: Programming Languages and Systems: 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 \u2013 April 1, 2021, Proceedings, pp. 118\u2013147. Springer-Verlag, Berlin (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_5","DOI":"10.1007\/978-3-030-72019-3_5"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D.: Infer: an automatic program verifier for memory safety of C programs. In: Proceedings of the Third International Conference on NASA Formal Methods, NFM\u201911, pp. 459\u2013465. Springer-Verlag, Berlin (2011)","DOI":"10.1007\/978-3-642-20398-5_33"},{"issue":"1","key":"10_CR4","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/s10817-018-9457-5","volume":"61","author":"Q Cao","year":"2018","unstructured":"Cao, Q., Beringer, L., Gruetter, S., Dodds, J., Appel, A.W.: VST-Floyd: a separation logic tool to verify correctness of C programs. J. Autom. Reason. 61(1), 367\u2013422 (2018). https:\/\/doi.org\/10.1007\/s10817-018-9457-5","journal-title":"J. Autom. Reason."},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"Chin, W.N., David, C., Nguyen, H.H., Qin, S.: multiple pre\/post specifications for heap-manipulating methods. In: 10th IEEE High Assurance Systems Engineering Symposium (HASE\u201907), pp. 357\u2013364 (2007). https:\/\/doi.org\/10.1109\/HASE.2007.19","DOI":"10.1109\/HASE.2007.19"},{"issue":"3","key":"10_CR6","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1016\/0097-3165(73)90004-6","volume":"14","author":"GB Dantzig","year":"1973","unstructured":"Dantzig, G.B., Curtis Eaves, B.: Fourier-Motzkin elimination and its dual. J. Comb. Theory, Ser. A 14(3), 288\u2013297 (1973). https:\/\/doi.org\/10.1016\/0097-3165(73)90004-6","journal-title":"J. Comb. Theory, Ser. A"},{"key":"10_CR7","unstructured":"Facebook: SPARTA: a library of software components designed for building high-performance static analyzers based on the theory of abstract interpretation. https:\/\/github.com\/facebook\/SPARTA. gitHub repository"},{"key":"10_CR8","unstructured":"Huawei LiteOS: LiteOS kernel. https:\/\/github.com\/LiteOS\/LiteOS"},{"key":"10_CR9","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-319-57288-8_15","volume-title":"NASA Formal Methods","author":"H Illous","year":"2017","unstructured":"Illous, H., Lemerre, M., Rival, X.: A relational shape abstract domain. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NASA Formal Methods, pp. 212\u2013229. Springer International Publishing, Cham (2017)"},{"key":"10_CR10","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods, pp. 41\u201355. Springer, Berlin, Heidelberg (2011)"},{"issue":"9","key":"10_CR11","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/3022670.2951943","volume":"51","author":"R Jung","year":"2016","unstructured":"Jung, R., Krebbers, R., Birkedal, L., Dreyer, D.: Higher-order ghost state. SIGPLAN Not. 51(9), 256\u2013269 (2016). https:\/\/doi.org\/10.1145\/3022670.2951943","journal-title":"SIGPLAN Not."},{"issue":"3","key":"10_CR12","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Cuoq, P., Correnson, L., Prevosto, V., Signoles, J.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573\u2013609 (2015). https:\/\/doi.org\/10.1007\/s00165-014-0326-7","journal-title":"Formal Aspects Comput."},{"key":"10_CR13","unstructured":"Kroening, D., Schrammel, P., Tautschnig, M.: CBMC: the C bounded model checker (2023). https:\/\/arxiv.org\/abs\/2302.02384"},{"key":"10_CR14","volume-title":"Decision Procedures: An Algorithmic Point of View","author":"D Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, 1st edn. Springer Publishing Company, Incorporated, Cham (2008)","edition":"1"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) Verification, Model Checking, and Abstract Interpretation (VMCAI). LNCS, vol.\u00a09583, pp. 41\u201362. Springer-Verlag (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"10_CR16","unstructured":"Nguyen, H.H., David, C., Qin, S., Chin, W.N.: Automated verification of shape and size properties via separation logic. In: Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI\u201907, pp. 251\u2013266. Springer-Verlag, Berlin (2007)"},{"key":"10_CR17","unstructured":"Nguyen, Q.L., David, C., Chin, W.N.: Hip\/Sleek: verification system for heap-manipulating programs (Splice example) (2023). https:\/\/github.com\/hipsleek\/hipsleek\/blob\/master\/benchmark\/SV-COMP\/list_properties\/splice.ss. gitHub repository, benchmark example: splice.ss"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Oliveras, A.: Proof-producing congruence closure. In: Proceedings of the 16th International Conference on Term Rewriting and Applications,. RTA\u201905, pp. 453\u2013468 Springer-Verlag, Berlin (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_33","DOI":"10.1007\/978-3-540-32033-3_33"},{"key":"10_CR19","doi-asserted-by":"publisher","unstructured":"Pulte, C., Makwana, D.C., Sewell, T., Memarian, K., Sewell, P., Krishnaswami, N.: CN: verifying systems C code with separation-logic refinement types. Proc. ACM Program. Lang. 7(POPL) (2023). https:\/\/doi.org\/10.1145\/3571194","DOI":"10.1145\/3571194"},{"key":"10_CR20","doi-asserted-by":"publisher","unstructured":"Sammler, M., Lepigre, R., Krebbers, R., Memarian, K., Dreyer, D., Garg, D.: RefinedC: automating the foundational verification of C code with refined ownership types. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021), pp. 158\u2013174. ACM, New York (2021). https:\/\/doi.org\/10.1145\/3453483.3454060","DOI":"10.1145\/3453483.3454060"},{"key":"10_CR21","unstructured":"Wang, Z., et al.: Stellis: a strategy language for purifying separation logic entailments (2025). https:\/\/arxiv.org\/abs\/2512.05159"},{"key":"10_CR22","doi-asserted-by":"publisher","unstructured":"Wu, S., Wu, X., Cao, Q.: Encode the $$\\forall \\exists $$ relational Hoare logic into standard Hoare logic. Proc. ACM Program. Lang. 9(OOPSLA2) (2025). https:\/\/doi.org\/10.1145\/3763138","DOI":"10.1145\/3763138"},{"key":"10_CR23","unstructured":"Wu, X., et al.: QCP: a practical separation logic-based C program verification tool (2026). https:\/\/arxiv.org\/abs\/2505.12878"},{"key":"10_CR24","doi-asserted-by":"publisher","unstructured":"Zhou, L., Qin, J., Wang, Q., Appel, A.W., Cao, Q.: VST-A: a foundationally sound annotation verifier. Proc. ACM Program. Lang. 8(POPL) (2024). https:\/\/doi.org\/10.1145\/3632911","DOI":"10.1145\/3632911"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-30693-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,6]],"date-time":"2026-07-06T14:08:31Z","timestamp":1783346911000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-30693-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7,2]]},"ISBN":["9783032306920","9783032306937"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-30693-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,7,2]]},"assertion":[{"value":"2 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Theoretical Aspects of Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Shanghai","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tase2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tase2026.github.io\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}