{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T03:34:36Z","timestamp":1743132876076,"version":"3.40.3"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031308284"},{"type":"electronic","value":"9783031308291"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T00:00:00Z","timestamp":1682035200000},"content-version":"vor","delay-in-days":110,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>An efficient entailment proof system is essential to compositional verification using separation logic. Unfortunately, existing decision procedures are either inexpressive or inefficient. For example, Smallfoot is an efficient procedure but only works with hardwired lists and trees. Other procedures that can support general inductive predicates run exponentially in time as their proof search requires back-tracking to deal with a disjunction in the consequent.<\/jats:p><jats:p>This paper presents a decision procedure to derive cyclic entailment proofs for general inductive predicates in polynomial time. Our procedure is efficient and does not require back-tracking; it uses normalisation rules that help avoid the introduction of disjunction in the consequent. Moreover, our decidable fragment is sufficiently expressive: It is based on compositional predicates and can capture a wide range of data structures, including sorted and nested list segments, skip lists with fast-forward pointers, and binary search trees. We implemented the proposal in a prototype tool, called<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathtt {S2S_{Lin}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>S<\/mml:mi><mml:mn>2<\/mml:mn><mml:msub><mml:mi>S<\/mml:mi><mml:mi>Lin<\/mml:mi><\/mml:msub><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>, and evaluated it over challenging problems from a recent separation logic competition. The experimental results confirm the efficiency of the proposed system.<\/jats:p>","DOI":"10.1007\/978-3-031-30829-1_23","type":"book-chapter","created":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T19:56:19Z","timestamp":1682020579000},"page":"477-497","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic"],"prefix":"10.1007","author":[{"given":"Quang Loc","family":"Le","sequence":"first","affiliation":[]},{"given":"Xuan-Bach D.","family":"Le","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,4,21]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max Kanovich, and Jo\u00ebl Ouaknine. Foundations for decision problems in separation logic with general inductive predicates. In Anca Muscholl, editor, Foundations of Software Science and Computation Structures, pages 411\u2013425, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg.","key":"23_CR1","DOI":"10.1007\/978-3-642-54830-7_27"},{"doi-asserted-by":"crossref","unstructured":"J.\u00a0Berdine, C.\u00a0Calcagno, and P.\u00a0W. O\u2019Hearn. Symbolic Execution with Separation Logic. In APLAS, volume 3780, pages 52\u201368, November 2005.","key":"23_CR2","DOI":"10.1007\/11575467_5"},{"doi-asserted-by":"crossref","unstructured":"J.\u00a0Brotherston. Cyclic proofs for first-order logic with inductive definitions. In Proceedings of TABLEAUX-14, volume 3702 of LNAI, pages 78\u201392. Springer-Verlag, 2005.","key":"23_CR3","DOI":"10.1007\/11554554_8"},{"doi-asserted-by":"crossref","unstructured":"J.\u00a0Brotherston, N.\u00a0Gorogiannis, and R.\u00a0L. Petersen. A generic cyclic theorem prover. In Proceedings of APLAS-10, LNCS, pages 350\u2013367. Springer, 2012.","key":"23_CR4","DOI":"10.1007\/978-3-642-35182-2_25"},{"doi-asserted-by":"crossref","unstructured":"James Brotherston, Dino Distefano, and Rasmus\u00a0Lerchedahl Petersen. Automated cyclic entailment proofs in separation logic. In Proceedings of the 23rd International Conference on Automated Deduction, CADE\u201911, page 131\u2013146, Berlin, Heidelberg, 2011. Springer-Verlag.","key":"23_CR5","DOI":"10.1007\/978-3-642-22438-6_12"},{"doi-asserted-by":"crossref","unstructured":"Cristiano Calcagno, Dino Distefano, Jeremy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter O\u2019Hearn, Irene Papakonstantinou, Jim Purbrick, and Dulma Rodriguez. Moving fast with software verification. In Klaus Havelund, Gerard Holzmann, and Rajeev Joshi, editors, NASA Formal Methods, pages 3\u201311, Cham, 2015. Springer International Publishing.","key":"23_CR6","DOI":"10.1007\/978-3-319-17524-9_1"},{"doi-asserted-by":"crossref","unstructured":"Cristiano Calcagno, Dino Distefano, Peter\u00a0W. O\u2019Hearn, and Hongseok Yang. Compositional shape analysis by means of bi-abduction. In POPL, pages 289\u2013300, 2009.","key":"23_CR7","DOI":"10.1145\/1594834.1480917"},{"unstructured":"Taolue Chen, Fu\u00a0Song, and Zhilin Wu. Tractability of Separation Logic with Inductive Definitions: Beyond Lists. In Roland Meyer and Uwe Nestmann, editors, 28th International Conference on Concurrency Theory (CONCUR 2017), volume\u00a085 of Leibniz International Proceedings in Informatics (LIPIcs), pages 37:1\u201337:17, Dagstuhl, Germany, 2017. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik.","key":"23_CR8"},{"doi-asserted-by":"crossref","unstructured":"W.-N. Chin, C.\u00a0Gherghina, R.\u00a0Voicu, Q.-L. Le, F.\u00a0Craciun, and S.\u00a0Qin. A specialization calculus for pruning disjunctive predicates to support verification. In CAV. 2011.","key":"23_CR9","DOI":"10.1007\/978-3-642-22110-1_23"},{"doi-asserted-by":"crossref","unstructured":"Duc-Hiep Chu, Joxan Jaffar, and Minh-Thai Trinh. Automatic induction proofs of data-structures in imperative programs. In Proceedings of PLDI, PLDI \u201915, pages 457\u2013466, New York, NY, USA, 2015. ACM.","key":"23_CR10","DOI":"10.1145\/2813885.2737984"},{"doi-asserted-by":"crossref","unstructured":"B.\u00a0Cook, C.\u00a0Haase, J.\u00a0Ouaknine, M.\u00a0Parkinson, and J.\u00a0Worrell. Tractable reasoning in a fragment of separation logic. In CONCUR, volume 6901, pages 235\u2013249. 2011.","key":"23_CR11","DOI":"10.1007\/978-3-642-23217-6_16"},{"doi-asserted-by":"crossref","unstructured":"Christopher Curry, Quang\u00a0Loc Le, and Shengchao Qin. Bi-abductive inference for shape and ordering properties. In 2019 24th International Conference on Engineering of Complex Computer Systems (ICECCS), pages 220\u2013225, 2019.","key":"23_CR12","DOI":"10.1109\/ICECCS.2019.00031"},{"doi-asserted-by":"crossref","unstructured":"Dino Distefano, Manuel F\u00e4hndrich, Francesco Logozzo, and Peter\u00a0W. O\u2019Hearn. Scaling static analyses at facebook. Commun. ACM, 62(8):62\u201370, jul 2019.","key":"23_CR13","DOI":"10.1145\/3338112"},{"doi-asserted-by":"crossref","unstructured":"Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Unifying decidable entailments in separation logic with inductive definitions. In Automated Deduction-CADE 28-28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, pages 183\u2013199, 2021.","key":"23_CR14","DOI":"10.1007\/978-3-030-79876-5_11"},{"doi-asserted-by":"crossref","unstructured":"Constantin Enea, Ondrej Leng\u00e1l, Mihaela Sighireanu, and Tom\u00e1s Vojnar. Compositional entailment checking for a fragment of separation logic. Formal Methods in System Design, 51(3):575\u2013607, 2017.","key":"23_CR15","DOI":"10.1007\/s10703-017-0289-4"},{"unstructured":"Constantin Enea, Mihaela Sighireanu, and Zhilin Wu. On automated lemma generation for separation logic with inductive definitions. ATVA, 2015.","key":"23_CR16"},{"doi-asserted-by":"crossref","unstructured":"Xincai Gu, Taolue Chen, and Zhilin Wu. A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints, pages 532\u2013549. Springer International Publishing, Cham, 2016.","key":"23_CR17","DOI":"10.1007\/978-3-319-40229-1_36"},{"doi-asserted-by":"crossref","unstructured":"R.\u00a0Iosif, A.\u00a0Rogalewicz, and J.\u00a0Sim\u00e1cek. The tree width of separation logic with recursive definitions. In CADE, pages 21\u201338, 2013.","key":"23_CR18","DOI":"10.1007\/978-3-642-38574-2_2"},{"doi-asserted-by":"crossref","unstructured":"Radu Iosif, Adam Rogalewicz, and Tom\u00e1s Vojnar. Deciding entailments in inductive separation logic with tree automata. ATVA, 2014.","key":"23_CR19","DOI":"10.1007\/978-3-319-11936-6_15"},{"doi-asserted-by":"crossref","unstructured":"S.\u00a0Ishtiaq and P.W. O\u2019Hearn. BI as an assertion language for mutable data structures. In ACM POPL, pages 14\u201326, London, January 2001.","key":"23_CR20","DOI":"10.1145\/373243.375719"},{"doi-asserted-by":"crossref","unstructured":"Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, and Florian Zuleger. Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic, pages 611\u2013638. Springer Berlin Heidelberg, Berlin, Heidelberg, 2017.","key":"23_CR21","DOI":"10.1007\/978-3-662-54434-1_23"},{"doi-asserted-by":"crossref","unstructured":"Katelaan Jens, Jovanovic Dejan, and Weissenbacher Georg. A separation logic with data: Small models and automation. In IJCAI, 2018.","key":"23_CR22","DOI":"10.1007\/978-3-319-94205-6_30"},{"doi-asserted-by":"crossref","unstructured":"Jens Katelaan, Christoph Matheja, and Florian Zuleger. Effective entailment checking for separation logic with inductive definitions. In Tom\u00e1\u0161 Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 319\u2013336, Cham, 2019. Springer International Publishing.","key":"23_CR23","DOI":"10.1007\/978-3-030-17465-1_18"},{"doi-asserted-by":"crossref","unstructured":"Quang\u00a0Loc Le. Compositional satisfiability solving in separation logic. In Fritz Henglein, Sharon Shoham, and Yakir Vizel, editors, Verification, Model Checking, and Abstract Interpretation, pages 578\u2013602, Cham, 2021. Springer International Publishing.","key":"23_CR24","DOI":"10.1007\/978-3-030-67067-2_26"},{"doi-asserted-by":"crossref","unstructured":"Quang\u00a0Loc Le, Cristian Gherghina, Shengchao Qin, and Wei-Ngan Chin. Shape analysis via second-order bi-abduction. In CAV, volume 8559, pages 52\u201368. 2014.","key":"23_CR25","DOI":"10.1007\/978-3-319-08867-9_4"},{"doi-asserted-by":"crossref","unstructured":"Quang\u00a0Loc Le and Mengda He. A decision procedure for string logic with quadratic equations, regular expressions and length constraints. In Sukyoung Ryu, editor, Programming Languages and Systems, pages 350\u2013372, Cham, 2018. Springer International Publishing.","key":"23_CR26","DOI":"10.1007\/978-3-030-02768-1_19"},{"doi-asserted-by":"publisher","unstructured":"Quang\u00a0Loc Le and Xuan-Bach\u00a0D. Le. Artifact for an efficient cyclic entailment procedure in a fragment of separation logic, February 2023. https:\/\/doi.org\/10.5281\/zenodo.7619870.","key":"23_CR27","DOI":"10.5281\/zenodo.7619870"},{"unstructured":"Quang\u00a0Loc Le and Xuan-Bach\u00a0D. Le. An efficient cyclic entailment procedure in a fragment of separation logic, January 2023. Technical Report.","key":"23_CR28"},{"unstructured":"Quang\u00a0Loc Le, Jun Sun, and Wei-Ngan Chin. Satisfiability modulo heap-based programs. In CAV. 2016.","key":"23_CR29"},{"doi-asserted-by":"crossref","unstructured":"Quang\u00a0Loc Le, Jun Sun, and Shengchao Qin. Frame inference for inductive entailment proofs in separation logic. In Dirk Beyer and Marieke Huisman, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 41\u201360, 2018.","key":"23_CR30","DOI":"10.1007\/978-3-319-89960-2_3"},{"doi-asserted-by":"crossref","unstructured":"Quang\u00a0Loc Le, Makoto Tatsuta, Jun Sun, and Wei-Ngan Chin. A decidable fragment in separation logic with inductive predicates and arithmetic. In CAV, pages 495\u2013517, 2017.","key":"23_CR31","DOI":"10.1007\/978-3-319-63390-9_26"},{"doi-asserted-by":"crossref","unstructured":"Scott McPeak and George\u00a0C. Necula. Data structure specifications via local equality axioms. In Kousha Etessami and Sriram\u00a0K. Rajamani, editors, Computer Aided Verification, pages 476\u2013490, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg.","key":"23_CR32","DOI":"10.1007\/11513988_47"},{"doi-asserted-by":"crossref","unstructured":"Juan\u00a0Antonio Navarro\u00a0P\u00e9rez and Andrey Rybalchenko. Separation logic + superposition calculus = heap theorem prover. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201911, page 556\u2013566, New York, NY, USA, 2011. Association for Computing Machinery.","key":"23_CR33","DOI":"10.1145\/1993498.1993563"},{"doi-asserted-by":"crossref","unstructured":"Juan Antonio Navarro\u00a0P\u00e9rez and Andrey Rybalchenko. Separation logic modulo theories. In APLAS, volume 8301, pages 90\u2013106. 2013.","key":"23_CR34","DOI":"10.1007\/978-3-319-03542-0_7"},{"doi-asserted-by":"crossref","unstructured":"R.\u00a0Piskac, T.\u00a0Wies, and D.\u00a0Zufferey. Automating separation logic using smt. In Natasha Sharygina and Helmut Veith, editors, CAV, volume 8044, pages 773\u2013789. 2013.","key":"23_CR35","DOI":"10.1007\/978-3-642-39799-8_54"},{"doi-asserted-by":"crossref","unstructured":"Ruzica Piskac, Thomas Wies, and Damien Zufferey. Automating separation logic with trees and data. In CAV, volume 8559, pages 711\u2013728. 2014.","key":"23_CR36","DOI":"10.1007\/978-3-319-08867-9_47"},{"unstructured":"J.\u00a0Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In IEEE LICS, pages 55\u201374, 2002.","key":"23_CR37"},{"unstructured":"Mihaela Sighireanu and Quang\u00a0Loc Le. SL-COMP 2022. https:\/\/sl-comp.github.io\/, 2022. [Online; accessed Jun-2022].","key":"23_CR38"},{"doi-asserted-by":"crossref","unstructured":"Mihaela Sighireanu, Juan Antonio\u00a0Navarro P\u00e9rez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds, Cristina Serban, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger, Wei-Ngan Chin, Quang\u00a0Loc Le, Quang-Trung Ta, Ton-Chanh Le, Thanh-Toan Nguyen, Siau-Cheng Khoo, Michal Cyprian, Adam Rogalewicz, Tom\u00e1s Vojnar, Constantin Enea, Ondrej Leng\u00e1l, Chong Gao, and Zhilin Wu. SL-COMP: competition of solvers for separation logic. In Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, pages 116\u2013132, 2019.","key":"23_CR39","DOI":"10.1007\/978-3-030-17502-3_8"},{"doi-asserted-by":"crossref","unstructured":"Quang-Trung Ta, Ton\u00a0Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin. Automated mutual explicit induction proof in separation logic. In John Fitzgerald, Constance Heitmeyer, Stefania Gnesi, and Anna Philippou, editors, FM 2016: Proceedings, pages 659\u2013676, 2016.","key":"23_CR40","DOI":"10.1007\/978-3-319-48989-6_40"},{"unstructured":"Quang-Trung Ta, Ton\u00a0Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin. Automated lemma synthesis in symbolic-heap separation logic. POPL, 2018.","key":"23_CR41"},{"doi-asserted-by":"crossref","unstructured":"Makoto Tatsuta, Koji Nakazawa, and Daisuke Kimura. Completeness of cyclic proofs for symbolic heaps with inductive definitions. In Anthony\u00a0Widjaja Lin, editor, Programming Languages and Systems, pages 367\u2013387, Cham, 2019. Springer International Publishing.","key":"23_CR42","DOI":"10.1007\/978-3-030-34175-6_19"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30829-1_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,18]],"date-time":"2024-10-18T22:42:42Z","timestamp":1729291362000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30829-1_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308284","9783031308291"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30829-1_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"21 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/fossacs","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":"85","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":"26","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":"0","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":"31% - 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.1","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":"10","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)"}}]}}