I've been wondering if it is possible to add a non-termination proof ability to IMP. I don't understand any of the existing methods used in provers like AProVE yet, but they seem to try to generate patterns rules/"shapes" which describe recurring behavior compactly, because an "infinite loop unroll" is not possible.
I don't know how to describe the following thought formally, but I'll try:
Most non-termination provers only seem to handle looping non-termination, which can be difficult enough. But the "shape" of non-looping non-terminating behavior can be arbitrarily complex. Existing provers only seem to be capable of generating/recognizing a limited set of "shapes" of behaviors - could some form of synthesis be used to define/explore more (or even all) of them?
In other words, it feels to me like if the types of pattern rules a prover supports is limited, it will never be able to find all forms of non-termination. Is it possible for some kind of "turing-complete-pattern-synthesis" to have a chance to encounter all possible non-halting patterns at least "in the limit"?
I've been wondering if it is possible to add a non-termination proof ability to IMP. I don't understand any of the existing methods used in provers like AProVE yet, but they seem to try to generate patterns rules/"shapes" which describe recurring behavior compactly, because an "infinite loop unroll" is not possible.
I don't know how to describe the following thought formally, but I'll try:
Most non-termination provers only seem to handle looping non-termination, which can be difficult enough. But the "shape" of non-looping non-terminating behavior can be arbitrarily complex. Existing provers only seem to be capable of generating/recognizing a limited set of "shapes" of behaviors - could some form of synthesis be used to define/explore more (or even all) of them?
In other words, it feels to me like if the types of pattern rules a prover supports is limited, it will never be able to find all forms of non-termination. Is it possible for some kind of "turing-complete-pattern-synthesis" to have a chance to encounter all possible non-halting patterns at least "in the limit"?