A Forward Analysis for Recurrent Sets

5 years 2 months ago
A Forward Analysis for Recurrent Sets
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 forward abstract interpretation–based analysis that can be used together ossibly complicated abstract domain where none of the above is readily available. The analysis searches for a recurrent set of every individual loop in a 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.
Alexey Bakhirkin, Josh Berdine, Nir Piterman
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where SAS
Authors Alexey Bakhirkin, Josh Berdine, Nir Piterman
Comments (0)