Seminar Details
2024-10-08 (14h) : Expanding Inductive Functional Proofs: Beyond Barrier Certificates
At Euler building (room A.002)
Organized by Mathematical Engineering
Speaker :
Majid Zamani (University of Colorado Boulder, USA)
Abstract :
A prominent approach to ensuring the safety of cyber-physical systems is through the use of barrier certificates—real-valued functions that serve as inductive proofs of safety. In this talk, we explore generalizations of barrier certificates, inspired by alternative notions of induction, to verify discrete-time dynamical systems against a wide range of specifications, from safety to more complex logic-based and security specifications. We introduce several new concepts, including k-inductive barrier certificates, closure certificates, and augmented barrier certificates, to verify systems against safety, ω-regular, and hyperproperty specifications. Drawing from k-induction in software verification, we propose k-inductive barrier certificates for system safety verification, allowing simpler functions to serve as proofs of safety compared to traditional barrier certificates. Building on the concept of transition invariants, we introduce closure certificates for verifying systems against ω-regular properties—temporal specifications described by ω-regular automata, which extend beyond safety to encompass a broader class of system behaviors. Finally, we present augmented barrier certificates for verifying systems against hyperproperties, which describe relationships between system traces and often address security-related concerns.