@inproceedings{10903,
  abstract     = {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.},
  author       = {Bouajjani, Ahmed and Dragoi, Cezara and Enea, Constantin and Sighireanu, Mihaela},
  booktitle    = {Automated Technology for Verification and Analysis},
  isbn         = {9783642333859},
  issn         = {1611-3349},
  location     = {Thiruvananthapuram, India},
  pages        = {167--182},
  publisher    = {Springer},
  title        = {{Accurate invariant checking for programs manipulating lists and arrays with infinite data}},
  doi          = {10.1007/978-3-642-33386-6_14},
  volume       = {7561},
  year         = {2012},
}

@inbook{5745,
  author       = {Gupta, Ashutosh},
  booktitle    = {Automated Technology for Verification and Analysis},
  isbn         = {9783642333859},
  issn         = {1611-3349},
  location     = {Thiruvananthapuram, Kerala, India},
  pages        = {107--121},
  publisher    = {Springer Berlin Heidelberg},
  title        = {{Improved Single Pass Algorithms for Resolution Proof Reduction}},
  doi          = {10.1007/978-3-642-33386-6_10},
  volume       = {7561},
  year         = {2012},
}