Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

PLDI

2011

ACM

2011

ACM

Program analysis and veriﬁcation 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/satisﬁability checking tools for separation logic is a challenging problem. In this paper, we present an efﬁcient, 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 ﬁrst-order reasoning with equality, as well as account for additional theories, e.g., linear arithmetic, using extensions of superpositi...

Added |
17 Sep 2011 |

Updated |
17 Sep 2011 |

Type |
Journal |

Year |
2011 |

Where |
PLDI |

Authors |
Juan Antonio Navarro Pérez, Andrey Rybalchenko |

Comments (0)