[{"status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","place":"Berlin, Heidelberg","type":"conference","date_published":"2012-10-15T00:00:00Z","publication_identifier":{"isbn":["9783642333859"],"eisbn":["9783642333866"],"issn":["0302-9743"],"eissn":["1611-3349"]},"language":[{"iso":"eng"}],"conference":{"end_date":"2012-10-06","location":"Thiruvananthapuram, India","start_date":"2012-10-03","name":"ATVA: Automated Technology for Verification and Analysis"},"publication":"Automated Technology for Verification and Analysis","month":"10","oa_version":"None","volume":7561,"acknowledgement":"This work has been partially supported by the French ANR project Veridyc","year":"2012","citation":{"ama":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. Accurate invariant checking for programs manipulating lists and arrays with infinite data. In: <i>Automated Technology for Verification and Analysis</i>. Vol 7561. LNCS. Berlin, Heidelberg: Springer; 2012:167-182. doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_14\">10.1007/978-3-642-33386-6_14</a>","apa":"Bouajjani, A., Dragoi, C., Enea, C., &#38; Sighireanu, M. (2012). Accurate invariant checking for programs manipulating lists and arrays with infinite data. In <i>Automated Technology for Verification and Analysis</i> (Vol. 7561, pp. 167–182). Berlin, Heidelberg: Springer. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_14\">https://doi.org/10.1007/978-3-642-33386-6_14</a>","chicago":"Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu. “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.” In <i>Automated Technology for Verification and Analysis</i>, 7561:167–82. LNCS. Berlin, Heidelberg: Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_14\">https://doi.org/10.1007/978-3-642-33386-6_14</a>.","ieee":"A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Accurate invariant checking for programs manipulating lists and arrays with infinite data,” in <i>Automated Technology for Verification and Analysis</i>, Thiruvananthapuram, India, 2012, vol. 7561, pp. 167–182.","short":"A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Automated Technology for Verification and Analysis, Springer, Berlin, Heidelberg, 2012, pp. 167–182.","mla":"Bouajjani, Ahmed, et al. “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.” <i>Automated Technology for Verification and Analysis</i>, vol. 7561, Springer, 2012, pp. 167–82, doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_14\">10.1007/978-3-642-33386-6_14</a>.","ista":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Accurate invariant checking for programs manipulating lists and arrays with infinite data. Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and AnalysisLNCS, LNCS, vol. 7561, 167–182."},"date_updated":"2023-09-05T14:07:24Z","abstract":[{"text":"We propose a logic-based framework for automated reasoning about sequential programs manipulating singly-linked lists and arrays with unbounded data. We introduce the logic SLAD, which allows combining shape constraints, written in a fragment of Separation Logic, with data and size constraints. We address the problem of checking the entailment between SLAD formulas, which is crucial in performing pre-post condition reasoning. Although this problem is undecidable in general for SLAD, we propose a sound and powerful procedure that is able to solve this problem for a large class of formulas, beyond the capabilities of existing techniques and tools. We prove that this procedure is complete, i.e., it is actually a decision procedure for this problem, for an important fragment of SLAD including known decidable logics. We implemented this procedure and shown its preciseness and its efficiency on a significant benchmark of formulas.","lang":"eng"}],"day":"15","doi":"10.1007/978-3-642-33386-6_14","quality_controlled":"1","series_title":"LNCS","page":"167-182","publisher":"Springer","author":[{"last_name":"Bouajjani","first_name":"Ahmed","full_name":"Bouajjani, Ahmed"},{"id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","first_name":"Cezara","last_name":"Dragoi","full_name":"Dragoi, Cezara"},{"full_name":"Enea, Constantin","last_name":"Enea","first_name":"Constantin"},{"full_name":"Sighireanu, Mihaela","last_name":"Sighireanu","first_name":"Mihaela"}],"scopus_import":"1","_id":"10903","intvolume":"      7561","alternative_title":["LNCS"],"title":"Accurate invariant checking for programs manipulating lists and arrays with infinite data","department":[{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2022-03-21T07:58:39Z","publication_status":"published"},{"publisher":"Springer Berlin Heidelberg","file_date_updated":"2020-07-14T12:47:10Z","ec_funded":1,"quality_controlled":"1","series_title":"LNCS","page":"107-121","intvolume":"      7561","title":"Improved Single Pass Algorithms for Resolution Proof Reduction","pubrep_id":"180","date_created":"2018-12-18T13:01:46Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","publication_status":"published","author":[{"full_name":"Gupta, Ashutosh","last_name":"Gupta","first_name":"Ashutosh"}],"_id":"5745","ddc":["005"],"volume":7561,"doi":"10.1007/978-3-642-33386-6_10","citation":{"ista":"Gupta A. 2012.Improved Single Pass Algorithms for Resolution Proof Reduction. In: Automated Technology for Verification and Analysis. vol. 7561, 107–121.","mla":"Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.” <i>Automated Technology for Verification and Analysis</i>, vol. 7561, Springer Berlin Heidelberg, 2012, pp. 107–21, doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">10.1007/978-3-642-33386-6_10</a>.","short":"A. Gupta, in:, Automated Technology for Verification and Analysis, Springer Berlin Heidelberg, Berlin, Heidelberg, 2012, pp. 107–121.","ieee":"A. Gupta, “Improved Single Pass Algorithms for Resolution Proof Reduction,” in <i>Automated Technology for Verification and Analysis</i>, vol. 7561, Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, pp. 107–121.","chicago":"Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.” In <i>Automated Technology for Verification and Analysis</i>, 7561:107–21. LNCS. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">https://doi.org/10.1007/978-3-642-33386-6_10</a>.","ama":"Gupta A. Improved Single Pass Algorithms for Resolution Proof Reduction. In: <i>Automated Technology for Verification and Analysis</i>. Vol 7561. LNCS. Berlin, Heidelberg: Springer Berlin Heidelberg; 2012:107-121. doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">10.1007/978-3-642-33386-6_10</a>","apa":"Gupta, A. (2012). Improved Single Pass Algorithms for Resolution Proof Reduction. In <i>Automated Technology for Verification and Analysis</i> (Vol. 7561, pp. 107–121). Berlin, Heidelberg: Springer Berlin Heidelberg. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">https://doi.org/10.1007/978-3-642-33386-6_10</a>"},"year":"2012","date_updated":"2023-09-05T14:15:29Z","conference":{"start_date":"2012-10-03","name":"ATVA 2012","end_date":"2012-10-06","location":"Thiruvananthapuram, Kerala, India"},"language":[{"iso":"eng"}],"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"}],"oa_version":"None","has_accepted_license":"1","publication":"Automated Technology for Verification and Analysis","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","place":"Berlin, Heidelberg","file":[{"date_created":"2018-12-18T13:07:35Z","file_size":465502,"checksum":"68415837a315de3cc4d120f6019d752c","date_updated":"2020-07-14T12:47:10Z","content_type":"application/pdf","file_name":"2012_ATVA_Gupta.pdf","access_level":"open_access","relation":"main_file","file_id":"5746","creator":"dernst"}],"oa":1,"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783642333859","9783642333866"]},"type":"book_chapter","date_published":"2012-01-01T00:00:00Z"}]