Please use this identifier to cite or link to this item:
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: Finding Recurrent Sets with Backward Analysis and Trace Partitioning. In: Chechik M., Raskin JF. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2016. Lecture Notes in Computer Science, vol 9636.
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: 10.1007/978-3-662-49674-9_2
ISSN: 0302-9743
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.
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.