MINDS @ UW-Madison

Abstraction Refinement for 3-Valued Logic Analysis

Show simple item record


Files Size Format View
TR1504.pdf 2.319Mb application/pdf View/Open
Key Value Language
dc.contributor.author Loginov, Alexey en_US
dc.contributor.author Reps, Thomas en_US
dc.contributor.author Sagiv, Mooly en_US
dc.date.accessioned 2012-03-15T17:18:10Z
dc.date.available 2012-03-15T17:18:10Z
dc.date.created 2004 en_US
dc.date.issued 2004
dc.identifier.citation TR1504 en_US
dc.identifier.uri http://digital.library.wisc.edu/1793/60396
dc.description.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. en_US
dc.description.provenance Create and issued dates reconciled by Wendt Commons staff on 8-29-2014 (AF) en_US
dc.description.provenance Made available in DSpace on 2012-03-15T17:18:10Z (GMT). No. of bitstreams: 1 TR1504.pdf: 2319476 bytes, checksum: 334376d3ebe29c47162f66ea048fa984 (MD5) en
dc.format.mimetype application/pdf en_US
dc.publisher University of Wisconsin-Madison Department of Computer Sciences en_US
dc.title Abstraction Refinement for 3-Valued Logic Analysis en_US
dc.type Technical Report en_US

Part of

Show simple item record