Efficient CTL Verification via Horn Constraints Solving

Tewodros A. Beyene, Corneliu Popeea, Andrey Rybalchenko

The use of temporal logics has long been recognised as a fundamental approach to the formal specification and verification of reactive systems. In this paper, we take on the proble…