Show simple item record

dc.contributor.authorThakur, Aditya
dc.contributor.authorBreck, Jason
dc.contributor.authorReps, Thomas
dc.description.abstractSeparation logic is an expressive logic for reasoning about heap structures in programs. This paper presents a semi-decision procedure for checking unsatisfiability of formulas in a fragment of separation logic that includes points-to assertions (x |-> y), acyclic-list-segment assertions (ls(x,y)), logical-and, logical-or, separating conjunction, and septraction (the DeMorgan-dual of separating implication). The fragment that we consider allows negation at leaves, and includes formulas that lie outside other separation-logic fragments considered in the literature. The semi-decision procedure is designed using concepts from abstract interpretation. The procedure uses an abstract domain of shape graphs to represent a set of heap structures, and computes an abstraction that over-approximates the set of satisfying models of a given formula. If the over-approximation is empty, then the formula is unsatisfiable. We have implemented the method, and evaluated it on a set of formulas taken from the literature. The implementation is able to establish the unsatisfiability of formulas that cannot be handled by previous approaches.en
dc.publisherUniversity of Wisconsin-Madison Department of Computer Sciences
dc.relation.replacesTR1800 (
dc.subjectabstract interpretationen
dc.subjectseparation logicen
dc.subjectsemi-decision procedureen
dc.subjectcanonical abstractionen
dc.titleSatisfiability Modulo Abstraction for Separation Logic with Linked Listsen
dc.typeTechnical Reporten

Files in this item


This item appears in the following Collection(s)

  • CS Technical Reports
    Technical Reports Archive for the Department of Computer Sciences at the University of Wisconsin-Madison

Show simple item record