About This Item

Ask the MINDS@UW Librarian

Abstraction Refinement for 3-Valued Logic Analysis

Show full item record

File(s):

Author(s)
Loginov, Alexey; Reps, Thomas; Sagiv, Mooly
Publisher
University of Wisconsin-Madison Department of Computer Sciences
Date
Mar 15, 2012
Abstract
This 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.
Permanent link
http://digital.library.wisc.edu/1793/60396 
Export
Export to RefWorks 
‚Äč

Part of

Show full item record

Search and browse




About MINDS@UW

Deposit materials

  1. Register to deposit in MINDS@UW
  2. Need deposit privileges? Contact us.
  3. Already registered? Have deposit privileges? Deposit materials.