eprintid: 1360944
rev_number: 37
eprint_status: archive
userid: 608
dir: disk0/01/36/09/44
datestamp: 2012-09-12 21:04:28
lastmod: 2021-09-26 22:10:40
status_changed: 2014-04-11 13:27:22
type: proceedings_section
metadata_visibility: show
item_issues_count: 0
creators_name: Navarro Pérez, JA
creators_name: Rybalchenko, A
title: Separation logic + superposition calculus = heap theorem prover
ispublished: pub
divisions: UCL
divisions: B04
divisions: C05
divisions: F48
note: This is the authors' accepted version of this published article. 
abstract: Program analysis and verification tools crucially depend on the ability to symbolically describe and reason about sets of program behaviors. Separation logic provides a promising foundation for dealing with heap manipulating programs, while the development of practical automated deduction/satisfiability checking tools for separation logic is a challenging problem. In this paper, we present an efficient, sound and complete automated theorem prover for checking validity of entailments between separation logic formulas with list segment predicates. Our theorem prover integrates separation logic inference rules that deal with list segments and a superposition calculus to deal with equality/aliasing between memory locations. The integration follows a modular combination approach that allows one to directly incorporate existing advanced techniques for first-order reasoning with equality, as well as account for additional theories, e.g., linear arithmetic, using extensions of superposition. An experimental evaluation of our entailment prover indicates speedups of several orders of magnitude with respect to the available state-of-the-art tools. © 2011 ACM.
date: 2011-06-04
official_url: http://dx.doi.org/10.1145/1993498.1993563
vfaculties: VENG
oa_status: green
full_text_type: other
language: eng
primo: open
primo_central: open_green
verified: verified_manual
elements_source: Scopus
elements_id: 437291
doi: 10.1145/1993498.1993563
isbn_13: 978-1-4503-0663-8
lyricists_name: Navarro Perez, Juan
lyricists_id: JANAV96
full_text_status: public
pagerange: 556 - 566
book_title: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
citation:        Navarro Pérez, JA;    Rybalchenko, A;      (2011)    Separation logic + superposition calculus = heap theorem prover.                     In:  Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI).  (pp. 556 - 566).         Green open access   
 
document_url: https://discovery.ucl.ac.uk/id/eprint/1360944/1/Navarro_Perez_ACM_pldi11.pdf