We are happy to present Ehsan Goharshady’s talk titled “From Termination to LTL: A template-based approach”.
The termination problem, also known as the halting problem, is known to be undecidable. This has motivated computer scientists to study proof rules for termination of restricted classes of programs. One such technique is ranking function generation, where we try to calculate an upper-bound on the number of steps the program takes to terminate from each configuration. In this talk, I briefly introduce how such ranking functions can be generated and how they can be extended to proof rules for verification of more general classes of specifications.
Ehsan Goharshady is a third-year PhD student at ISTA in Krishnendu Chatterjee’s group. He joined ISTA in 2022 after completing his bachelor’s in pure mathematics and computer science in Iran. His main interests are verification and analysis of non-deterministic and probabilistic imperative programs, model checking robust MDPs and solving bidding games.