Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/36303
Title: Finding Recurrent Sets with Backward Analysis and Trace Partitioning
Authors: Piterman, Nir
Bakhirkin, Alexey
First Published: 3-Apr-2016
Presented at: 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2-8 April 2016, Eindhoven, The Netherlands.
Publisher: Springer Verlag
Citation: Proceedings of TACAS', LNCS, 2016
Abstract: We propose an abstract-interpretation-based analysis for recurrent sets. A recurrent set is a set of states from which the execution of a program cannot or might not (as in our case) escape. A recurrent set is a part of a program’s nontermination proof (that needs to be complemented by reachability analysis). We find recurrent sets by performing a potentially over-approximate backward analysis that produces an initial candidate. We then perform over-approximate forward analysis on the candidate to check and refine it and ensure soundness. In practice, the analysis relies on trace partitioning that predicts future paths through the program that non-terminating executions will take. Using our technique, we were able to find recurrent sets in many benchmarks found in the literature including some that, to our knowledge, cannot be handled by existing tools. In addition, we note that typically, analyses that search for recurrent sets are applied to linear under-approximations of programs or employ some form of non-approximate numeric reasoning. In contrast, our analysis uses standard abstract-interpretation techniques and is potentially applicable to a larger class of abstract domains (and therefore – programs).
Series/Report no.: Lecture Notes In Computer Science;9636
DOI Link: TBC
ISSN: TBC
Links: http://www.etaps.org/index.php/2016/tacas/tacas-accepted
http://link.springer.com/
http://hdl.handle.net/2381/36303
Embargo on file until: 3-Apr-2017
Version: Post-print
Type: Conference Paper
Rights: Copyright © Springer Verlag. Deposited with reference to the publisher’s archiving policy available on the SHERPA/RoMEO website 18/01/2016.
Description: The file is under embargo for 12 months from publication.
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

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


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