{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T17:05:52Z","timestamp":1761930352473,"version":"3.40.3"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572586"},{"type":"electronic","value":"9783031572593"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T00:00:00Z","timestamp":1712361600000},"content-version":"vor","delay-in-days":96,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Deductive verification tools can prove a large range of program properties, but often face issues on recursive data structures. Abstract interpretation tools based on separation logic and shape analysis can efficiently reason about such structures but cannot deal with so large classes of properties. This short paper presents an ongoing work on combining both techniques. We show how a deductive verifier for C programs, <jats:sc>Frama-C<\/jats:sc>\/<jats:sc>Wp<\/jats:sc>, can benefit from a shape analysis tool, <jats:sc>MemCAD<\/jats:sc>, where structural and separation properties proved in the latter become assumptions for the former. A case study on selected functions of the tpm2-tss library using linked lists confirms the interest of the approach.<\/jats:p>","DOI":"10.1007\/978-3-031-57259-3_14","type":"book-chapter","created":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T13:01:39Z","timestamp":1712322099000},"page":"280-289","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Combining Deductive Verification with Shape Analysis"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-4834-7126","authenticated-orcid":false,"given":"T\u00e9o","family":"Bernier","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0000-8540-1273","authenticated-orcid":false,"given":"Yani","family":"Ziani","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1557-2813","authenticated-orcid":false,"given":"Nikolai","family":"Kosmatov","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9301-7829","authenticated-orcid":false,"given":"Fr\u00e9d\u00e9ric","family":"Loulergue","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,6]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Blanchard, A., Kosmatov, N., Loulergue, F.: Logic against ghosts: Comparison of two proof approaches for a list module. In: 34th Symp. on Applied Computing, Software Verification and Testing Track (SAC-SVT\u201919). pp. 2186\u20132195. ACM (2019)","DOI":"10.1145\/3297280.3297495"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: Verification of parallel and concurrent software. In: 13th Int. Conf. on Integrated Formal Methods (iFM\u201917). LNCS, vol. 10510, pp. 102\u2013110. Springer (2017)","DOI":"10.1007\/978-3-319-66845-1_7"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: 12th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201906). LNCS, vol.\u00a03920, pp. 287\u2013302. Springer (2006)","DOI":"10.1007\/11691372_19"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: From pen-and-paper proofs to industrial tools. In: Computing and Software Science - State of the Art and Perspectives, LNCS, vol. 10000, pp. 345\u2013373. Springer (2019)","DOI":"10.1007\/978-3-319-91908-9_18"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"He, P., Westbrook, E., Carmer, B., Phifer, C., Robert, V., Smeltzer, K., Stefanescu, A., Tomb, A., Wick, A., Yacavone, M., Zdancewic, S.: A type system for extracting functional specifications from memory-safe imperative programs. Proc. ACM Program. Lang. 5, 1\u201329 (2021)","DOI":"10.1145\/3485512"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: A software analysis perspective. Formal Asp. Comput. 27(3), 573\u2013609 (2015)","DOI":"10.1007\/s00165-014-0326-7"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. In: 17th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201916). LNCS, vol.\u00a09583, pp. 41\u201362. Springer (2016)","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Philippaerts, P., M\u00fchlberg, J.T., Penninckx, W., Smans, J., Jacobs, B., Piessens, F.: Software verification with VeriFast: Industrial case studies. Science of Computer Programming 82, 77\u201397 (2014)","DOI":"10.1016\/j.scico.2013.01.006"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Piskac, R., Wies, T., Zufferey, D.: GRASShopper - complete heap verification with mixed specifications. In: 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201914). LNCS, vol.\u00a08413, pp. 124\u2013139. Springer (2014)","DOI":"10.1007\/978-3-642-54862-8_9"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Sotin, P., Rival, X.: Hierarchical shape abstraction of dynamic structures in static blocks. In: 10th Asian Symposium on Programming Languages and Systems (APLAS\u201912). LNCS, vol.\u00a07705, pp. 131\u2013147. Springer (2012)","DOI":"10.1007\/978-3-642-35182-2_10"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Ziani, Y., Kosmatov, N., Loulergue, F., Gracia\u00a0P\u00e9rez, D., Bernier, T.: Towards formal verification of a TPM software stack (2023), http:\/\/arxiv.org\/abs\/2307.16821","DOI":"10.1007\/978-3-031-47705-8_6"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57259-3_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T13:04:13Z","timestamp":1712322253000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57259-3_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572586","9783031572593"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57259-3_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"6 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/fase\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"34% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}