Mishel Carelli

Mishel Carelli, Orna Grumberg

This work proposes a novel approach for automatic verification and synthesis of infinite-state reactive programs with respect to ${CTL}^*$ specifications, based on translation to Existential Horn Clauses (EHCs). $CTL^*$ is a powerful temporal logic, which subsumes the temporal logics LTL and CTL, both widely used in specification, verification, and synthesis of complex systems. EHCs with its solver E-HSF, is an extension of Constrained Horn Clauses, which includes existential quantification as well as the power of handling well-foundedness. We develop the translation system \textit{Trans}, which given a verification problem consisting of a program $P$ and a specification $ϕ$, builds a set of EHCs which is satisfiable iff $P$ satisfies $ϕ$. We also develop a synthesis algorithm that given a program with holes in conditions and assignments, fills the holes so that the synthesized program satisfies the given $CTL^*$ specification. We prove that our verification and synthesis algorithms are both sound and relative complete. Finally, we present case studies to demonstrate the applicability of our algorithms for $CTL^*$ verification and synthesis.

Mishel Carelli

Linear-constraint loops are programs whose transition relation is specified by a system of linear inequalities. The termination problem asks, given a loop, whether it admits an infinite computation. Decidability of termination remains open for linear-constraint loops over integers, rationals, and reals. We focus on loops over integers and show that they are tightly connected to generalized Collatz sequences - integer sequences generated by maps that are linear on each residue class modulo a fixed natural number. We prove that termination of one-variable linear-constraint loops is decidable in polynomial time, provided a long-standing conjecture about generalized Collatz sequences holds. Conversely, we show that any decision procedure for one-variable loops would prove or refute specific instances of this conjecture, which remain open. Moreover, we show that if a one-variable loop has a cyclic trace, then it also has a cyclic trace of length at most two.