Please use this identifier to cite or link to this item:
Title: A Forward Analysis for Recurrent Sets
Authors: Bakhirkin, Alexey
Berdine, J.
Piterman, Nir
First Published: 2-Sep-2015
Presented at: 22nd International Symposium, STATIC ANALYSIS SYMPOSIUM (SAS) 2015, Saint-Malo, France
Start Date: 9-Sep-2015
End Date: 11-Sep-2015
Publisher: Springer-Verlag
Citation: Lecture Notes in Computer Science
Abstract: Non-termination of structured imperative programs is primarily due to infinite loops. An important class of non-terminating loop behaviors can be characterized using the notion of recurrent sets. A recurrent set is a set of states from which execution of the loop cannot or might not escape. Existing analyses that infer recurrent sets to our knowledge rely on one of: the combination of forward and backward analyses, quantifier elimination, or SMT-solvers. We propose a purely forward abstract interpretation–based analysis that can be used together with a possibly complicated abstract domain where none of the above is readily available. The analysis searches for a recurrent set of every individual loop in a program by building a graph of abstract states and analyzing it in a novel way. The graph is searched for a witness of a recurrent set that takes the form of what we call a recurrent component which is somewhat similar to the notion of an end component in a Markov decision process.
DOI Link: 10.1007/978-3-662-48288-9_17
ISSN: 0302-9743
ISBN: 978-3-662-48287-2
Version: Post-print
Status: Peer-reviewed
Type: Conference Paper
Rights: Archived with reference to SHERPA/RoMEO and publisher website.
Appears in Collections:Published Articles, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
sas15.pdfPost-review (final submitted)281.4 kBAdobe PDFView/Open

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