Liveness Verification and Synthesis: New Algorithms for Recursive Programs

Roland Meyer, Sebastian Muskalla, Elisabeth Neumann

We consider the problems of liveness verification and liveness synthesis for recursive programs. The liveness verification problem (LVP) is to decide whether a given omega-context-…