BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//project/author//NONSGML v1.0//EN
CALSCALE:GREGORIAN
BEGIN:VEVENT
DTEND:20220713T120000Z
UID:388994edafb3d5a74c932a4c7e1c37f0-306
DTSTAMP:19700101T120011Z
DESCRIPTION:Bridging control theoretic approaches with methods in formal verification via Induction
URL;VALUE=URI:https://www.csa.iisc.ac.in/newweb/event/306/bridging-control-theoretic-approaches-with-methods-in-formal-verification-via-induction/
SUMMARY: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?
DTSTART:20220713T120000Z
END:VEVENT
END:VCALENDAR