---
_id: '10903'
abstract:
- lang: eng
  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.
acknowledgement: This work has been partially supported by the French ANR project
  Veridyc
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ahmed
  full_name: Bouajjani, Ahmed
  last_name: Bouajjani
- first_name: Cezara
  full_name: Dragoi, Cezara
  id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
  last_name: Dragoi
- first_name: Constantin
  full_name: Enea, Constantin
  last_name: Enea
- first_name: Mihaela
  full_name: Sighireanu, Mihaela
  last_name: Sighireanu
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.
  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.'
  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>.
  short: A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Automated Technology
    for Verification and Analysis, Springer, Berlin, Heidelberg, 2012, pp. 167–182.
conference:
  end_date: 2012-10-06
  location: Thiruvananthapuram, India
  name: 'ATVA: Automated Technology for Verification and Analysis'
  start_date: 2012-10-03
date_created: 2022-03-21T07:58:39Z
date_published: 2012-10-15T00:00:00Z
date_updated: 2023-09-05T14:07:24Z
day: '15'
department:
- _id: ToHe
doi: 10.1007/978-3-642-33386-6_14
intvolume: '      7561'
language:
- iso: eng
month: '10'
oa_version: None
page: 167-182
place: Berlin, Heidelberg
publication: Automated Technology for Verification and Analysis
publication_identifier:
  eisbn:
  - '9783642333866'
  eissn:
  - 1611-3349
  isbn:
  - '9783642333859'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: Accurate invariant checking for programs manipulating lists and arrays with
  infinite data
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7561
year: '2012'
...
---
_id: '5745'
article_processing_charge: No
author:
- first_name: Ashutosh
  full_name: Gupta, Ashutosh
  last_name: Gupta
citation:
  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>'
  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>.'
  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.'
  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.
conference:
  end_date: 2012-10-06
  location: Thiruvananthapuram, Kerala, India
  name: ATVA 2012
  start_date: 2012-10-03
date_created: 2018-12-18T13:01:46Z
date_published: 2012-01-01T00:00:00Z
date_updated: 2023-09-05T14:15:29Z
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-642-33386-6_10
ec_funded: 1
file:
- access_level: open_access
  checksum: 68415837a315de3cc4d120f6019d752c
  content_type: application/pdf
  creator: dernst
  date_created: 2018-12-18T13:07:35Z
  date_updated: 2020-07-14T12:47:10Z
  file_id: '5746'
  file_name: 2012_ATVA_Gupta.pdf
  file_size: 465502
  relation: main_file
file_date_updated: 2020-07-14T12:47:10Z
has_accepted_license: '1'
intvolume: '      7561'
language:
- iso: eng
oa: 1
oa_version: None
page: 107-121
place: Berlin, Heidelberg
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
publication: Automated Technology for Verification and Analysis
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - '9783642333859'
  - '9783642333866'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Berlin Heidelberg
pubrep_id: '180'
quality_controlled: '1'
series_title: LNCS
status: public
title: Improved Single Pass Algorithms for Resolution Proof Reduction
type: book_chapter
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7561
year: '2012'
...