Seminars

View all Seminars  |  Download ICal for this event

Bridging control theoretic approaches with methods in formal verification via Induction

Series: Department Seminar

Speaker: Vishnu Murali

Date/Time: Jul 13 11:30:00

Location: CSA Seminar Hall (Room No. 254, First Floor)

Abstract:
Inductive invariants have been widely studied in the context of program verification. In many cases where one fails to show a property is inductive, one instead tries to use different notions of induction (such as double, mutual, $k$, and strong), and then tries to show the property is inductive according to these notions. Analogously, the notion of barrier certificates act as inductive guarantees of safety for discrete-time continuous space systems. Barrier certificates are functions over the state space of the system such that they are non-increasing as the system evolves. The search for these functions typically rely on first deciding on a fixed template (e.g. a fixed degree polynomial) and then solving a semidefinite program to search for such a function. When such a function cannot be found, one typically changes the template (by increasing the degree of the polynomial) and tries again. Inspired by the idea of $k$-induction we considered notions of $k$-inductive barrier certificates and showed that for a fixed degree one may still find $k$-inductive barrier certificates when standard barrier certificates could not be found. As future research, a few natural follow up questions arise: 1) What are the different notions of barrier certificates for the notions of induction? 2) In many cases where one is not able to show a property to be inductive on a program, one may add more details or change the program in some way to help show the inductive property, what is the analogous idea in the context of dynamical systems? Lastly, I shall consider the question in the other direction: What are some of the other areas where control theory may inform approaches to formal verification?

Speaker Bio:
Vishnu Murali is a PhD student in the Department of Computer Science at University of Colorado, Boulder. His interests are in verification and synthesis for cyber-physical systems.

Host Faculty: Deepak D'Souza