The advent of autonomous systems in mission-critical areas such as autonomous vehicles and medical devices has led to significant research in ensuring their correctness. A prominent approach to provide such guarantees is to use functions that act as inductive proofs. To automate the search for such functions, one typically fixes their template (e.g. polynomials of a fixed degree). The search for these functions can then be handled using optimization-based approaches to find suitable candidates within the template class. When one fails to find such a function, a common approach is to change the template (for example increase the degree of the polynomial) and try again. An alternative approach is to instead change what we induct over. In this talk, I will illustrate how different notions of induction can be used to provide guarantees for specifications that range from safety to privacy. Finally, I will discuss two directions for future work: first to ensure the accountability for such systems and second, to find automated approaches to search for other novel inductive proof rules.

Short Bio:
Vishnu Murali is a postdoctoral associate in the Department of Computer Science at the University of Colorado Boulder. He received his PhD degree from the University of Colorado Boulder, USA in 2024. The focus of his research is to provide guarantees for autonomous or cyber-physical systems against properties specified in logic or via automata. During his PhD, he received awards for his research from the department of Computer Science at the University of Colorado Boulder, and one of his papers was a finalist for the ACM SIGBED HSCC best paper award.