Majid Zamani

The increasing use of machine learning in safety-critical domains amplifies the risk of adversarial threats, especially data poisoning attacks that corrupt training data to degrade performance or induce unsafe behavior. Most existing defenses lack formal guarantees or rely on restrictive assumptions about the model class, attack type, extent of poisoning, or point-wise certification, limiting their practical reliability. This paper introduces a principled formal robustness certification framework that models gradient-based training as a discrete-time dynamical system (dt-DS) and formulates poisoning robustness as a formal safety verification problem. By adapting the concept of barrier certificates (BCs) from control theory, we introduce sufficient conditions to certify a robust radius ensuring that the terminal model remains safe under worst-case ${\ell }_{p}$-norm based poisoning. To make this practical, we parameterize BCs as neural networks trained on finite sets of poisoned trajectories. We further derive probably approximately correct (PAC) bounds by solving a scenario convex program (SCP), which yields a confidence lower bound on the certified robustness radius generalizing beyond the training set. Importantly, our framework also extends to certification against test-time attacks, making it the first unified framework to provide formal guarantees in both training and test-time attack settings. Experiments on MNIST, SVHN, CIFAR-10, and CIFAR-100 show that our approach certifies non-trivial perturbation budgets while being model-agnostic and requiring no prior knowledge of the attack or contamination level.

Diagnosability is a system theoretical property characterizing whether fault occurrences in a system can always be detected within a finite time. In this paper, we investigate the verification of diagnosability for cyber-physical systems with continuous state sets. We develop an abstraction-free and automata-based framework to verify (the lack of) diagnosability, leveraging a notion of hybrid barrier certificates. To this end, we first construct a ($\delta,K$)-deterministic finite automaton that captures the occurrence of faults targeted for diagnosis. Then, the verification of diagnosability property is converted into a safety verification problem over a product system between the automaton and the augmented version of the dynamical system. We demonstrate that this verification problem can be addressed by computing hybrid barrier certificates for the product system. To this end, we introduce two systematic methods, leveraging sum-of-squares programming and counter-example guided inductive synthesis to search for such certificates. Additionally, if the system is found to be diagnosable, we propose methodologies to construct a diagnoser to identify fault occurrences online. Finally, we showcase the effectiveness of our methods through a case study.

Provides society information that may include news, reviews or technical notes that should be of interest to practitioners and researchers.

Barrier certificates are real-valued functions used to formally verify the safety of dynamical systems. For systems with unknown dynamics, data-driven barrier certificates have been developed to guarantee safety using only a finite set of data. However, most existing methods rely on knowledge of Lipschitz bounds of the system and require a fine discretization of the state set, leading to high sample complexity. In this paper, we propose a novel data-driven framework for learning barrier certificates for unknown monotone systems. Our approach is based on a suitable embedding of barrier certificates into a higher-dimensional space. By leveraging interval analysis, this embedding enables us to establish data-driven safety certificates for monotone systems. Unlike existing methods, our framework is independent of Lipschitz continuity and quantization parameters of the state set, allowing for arbitrary state-space discretization and thereby alleviating extensive sampling requirements. To efficiently construct barrier certificates, we introduce suitable neural network architectures and train them using an appropriately designed loss function. We illustrate our approach through two case studies, demonstrating that our method successfully finds separable embedded barrier certificates while substantially reducing sample complexity compared to conventional neural barrier certificate methods, all while maintaining formal correctness guarantees.

In this work, we develop a scheme for constructing continuous approximations (referred to as abstractions) of a class of discrete-time control systems with partially unknown dynamics. The abstraction, itself a nonlinear discrete-time control system (preferably with a significantly lower dimension than the original one) can be used as a substitute in the controller design process. The technique consists of using data sampled from the concrete system to find a lower dimensional subspace of its state space (which we call the active subspace), and constructing an abstraction candidate using Gaussian process (GP) regression. We derive sufficient conditions under which the GP candidate is shown to be the abstraction of the original system while quantifying the error bound between the output of the abstraction and that of the concrete system. A numerical example is presented to illustrate the effectiveness of this approach.

This paper is concerned with path-complete barrier functions which offer a graph-based methodology for verifying safety properties in switched systems. The path-complete framework leverages algebraic (barrier functions) as well as combinatorial (graph) components to characterize a set of safety conditions for switched systems, thus offering high flexibility (two degrees of freedom) in searching for suitable safety certificates. In this paper, we do not propose any new safety criteria. Instead, we further investigate the role that the combinatorial component plays in the safety verification problem. First, we prove that path-completeness, which is a property on a graph that describes the switching sequences, is necessary to obtain a set of valid safety conditions. As a result, the path-complete framework is able to provide a complete characterization of safety conditions for switched systems. Furthermore, we provide a systematic methodology for comparing two path-complete graphs and the conservatism associated with the resulting safety conditions. Specifically, we prove that under some conditions, such as when there exists a simulation relation between two path-complete graphs, it is possible to conclude that one graph is always able to provide less conservative safety conditions than another, independent of the algebraic properties of the switched system and the template of the barrier function under consideration. Such a result paves the way for a systematic use of the path-complete framework with barrier functions, as one can then consistently choose the appropriate graph that provides less conservative safety conditions.