Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/28950
Title: Backward analysis via over-approximate abstraction and under-approximate subtraction
Authors: Piterman, Nir
Bakhirkin, Alexey
Berdine, Josh
First Published: 2014
Presented at: 21st International Static Analysis Symposium, Munich Germany
Start Date: 11-Sep-2014
End Date: 13-Sep-2014
Publisher: Springer
Citation: Lecture Notes in Computer Science
Abstract: We propose a novel approach for computing weakest liberal safe preconditions of programs. The standard approaches, which call for either under-approximation of a greatest fixed point, or complementation of a least fixed point, are often difficult to apply successfully. Our approach relies on a different decomposition of the weakest precondition of loops. We exchange the greatest fixed point for the computation of a least fixed point above a recurrent set, instead of the bottom element. Convergence is achieved using over-approximation, while in order to maintain soundness we use an under-approximating logical subtraction operation. Unlike general complementation, subtraction more easily allows for increased precision in case its arguments are related. The approach is not restricted to a specific abstract domain and we use it to analyze programs using the abstract domains of intervals and of 3-valued structures.
DOI Link: 10.1007/978-3-319-10936-7_3
ISSN: 0302-9743
Links: http://www.springer.com/computer/lncs?SGWID=0-164-0-0-0
http://hdl.handle.net/2381/28950
http://eapls.org/items/1303/#.U6woHbGZjJp
http://link.springer.com/chapter/10.1007/978-3-319-10936-7_3
Version: Post-print
Status: Peer-reviewed
Type: Conference Paper
Rights: Copyright © 2014, Springer Verlag. Deposited with reference to the publisher’s archiving policy available on the SHERPA/RoMEO website.
Description: The file associated with this record is embargoed until 12 months after the date of publication. The final published version may be available through the links above.
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
sas14.pdfPost-review (final submitted)234.54 kBUnknownView/Open


Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.