I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications - Separation Logic + Superposition Calculus = Heap Theorem Prover

Reference:

Andrey Rybalchenko and Juan Antonio Navarro. Separation logic + Superposition calculus = Heap theorem prover. In PLDI'11: Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and implementation, San Jose, CA, USA, 2011. ACM Press.

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.

Keywords:

Verification, Logic, Reasoning, Separation Logic, Superposition

Suggested BibTeX entry:

@inproceedings{PLDI11,
    address = {San Jose, CA, USA},
    author = {Andrey Rybalchenko and Juan Antonio Navarro},
    booktitle = {PLDI'11: Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and implementation},
    publisher = {ACM Press},
    title = {Separation Logic + {Superposition} Calculus = {Heap} Theorem Prover},
    year = {2011}
}

PDF (287 kB)
See navarroj.com ...
Slides