Show simple item record

dc.contributor.authorLoginov, Alexeyen_US
dc.contributor.authorReps, Thomasen_US
dc.contributor.authorSagiv, Moolyen_US
dc.description.abstractThis paper concerns the question of how to create abstractions that are useful for program analysis. It presents a method that refines an abstraction automatically for analysis problems in which the semantics of statements and the query of interest are expressed using logical formulas. Refinement is carried out by introducing new instrumentation relations (defined via logical formulas over core relations, which capture the basic properties of memory configurations). A tool that incorporates the algorithm has been implemented and applied to several algorithms that manipulate linked lists and binary-search trees. In all but a few cases, Ihe tool is able to demonstrate (i) the partial correctness of the algorithms, and (ii) that the algorithms possess additional properties--e.g., stability or antistability.en_US
dc.publisherUniversity of Wisconsin-Madison Department of Computer Sciencesen_US
dc.titleAbstraction Refinement for 3-Valued Logic Analysisen_US
dc.typeTechnical Reporten_US

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