CTL* Verification and Synthesis using Existential Horn Clauses

Mishel Carelli, Orna Grumberg

This work proposes a novel approach for automatic verification and synthesis of infinite-state reactive programs with respect to ${CTL}^{\ast }$ specifications, based on translation to E…