CTL* Verification and Synthesis using Existential Horn Clauses

Speaker: Mishel Carelli, Technion Israel Institute of Technology

Abstract: This talk presents a novel approach for automatic verification and synthesis of infinite-state 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 include existential quantification as well as the power of handling well-foundedness. We developed the translation system Trans, which given a verification problem consisting of a program P and a specification S, builds a set of EHCs which is satisfiable iff P satisfies S. We also developed 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.

Biography: Mishel Carelli is a Master's student in the Faculty of Mathematics at the Technion – Israel Institute of Technology. He received his Bachelor's degree in Mathematics from Saint Petersburg University (SPBU) in July 2023. His current work focuses on the applications of Horn Clauses in verification and synthesis.

Host: Prof. Natasha Sharygina