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.

• Type: Journal
• Year: 2015
• Where: SAS
• Authors: Alexey Bakhirkin, Josh Berdine, Nir Piterman
• Keywords: Formal Methods, SAS 2015