XPost: comp.theory, sci.logic

Determining whether a given program terminates is the
quintessential undecidable problem...

Conceptually, our method proves that a program terminates by computing a transition formula for each loop that over-approximates the behavior of
its body, and then proving that the corresponding relation admits no
infinite sequences...

An efficient algorithm for computing an 𝜔-regular expression that
recognizes the infinite paths through a control flow graph, which forms
the algorithmic foundation of our program analysis framework.

https://dl.acm.org/doi/pdf/10.1145/3453483.3454110

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)