149 citations · 206 across the 29 of their papers we have counts for
34 papers
Extracting Forward Invariant Sets from Neural Network-Based Control Barrier Functions
Goli Vaisi, James Ferlez, Yasser Shoukry
Training Neural Networks (NNs) to serve as Barrier Functions (BFs) is a popular way to improve the safety of autonomous dynamical systems. Despite significant practical success, th…
Passivity Tools for Hybrid Learning Rules in Large Populations
Jair Certorio, Kevin Chang, Nuno C. Martins +2
Recent work has pioneered the use of system-theoretic passivity to study equilibrium stability for the dynamics of noncooperative strategic interactions in large populations of lea…
DeepBern-Nets: Taming the Complexity of Certifying Neural Networks using Bernstein Polynomial Activations and Precise Bound Propagation
Haitham Khedr, Yasser Shoukry
Formal certification of Neural Networks (NNs) is crucial for ensuring their safety, fairness, and robustness. Unfortunately, on the one hand, sound and complete certification algor…
Model Extraction Attacks Against Reinforcement Learning Based Controllers
Momina Sajid, Yanning Shen, Yasser Shoukry
We introduce the problem of model-extraction attacks in cyber-physical systems in which an attacker attempts to estimate (or extract) the feedback controller of the system. Extract…
SEO: Safety-Aware Energy Optimization Framework for Multi-Sensor Neural Controllers at the Edge
Mohanad Odema, James Ferlez, Yasser Shoukry +1
Runtime energy management has become quintessential for multi-sensor autonomous systems at the edge for achieving high performance given the platform constraints. Typical for such…
EnergyShield: Provably-Safe Offloading of Neural Network Controllers for Energy Efficiency
Mohanad Odema, James Ferlez, Goli Vaisi +2
To mitigate the high energy demand of Neural Network (NN) based Autonomous Driving Systems (ADSs), we consider the problem of offloading NN controllers from the ADS to nearby edge-…
BERN-NN: Tight Bound Propagation For Neural Networks Using Bernstein Polynomial Interval Arithmetic
Wael Fatnassi, Haitham Khedr, Valen Yamamoto +1
In this paper, we present BERN-NN as an efficient tool to perform bound propagation of Neural Networks (NNs). Bound propagation is a critical step in wide range of NN model checker…
Neurosymbolic Motion and Task Planning for Linear Temporal Logic Tasks
Xiaowu Sun, Yasser Shoukry
This paper presents a neurosymbolic framework to solve motion planning problems for mobile robots involving temporal goals. The temporal goals are described using temporal logic fo…
Polynomial-Time Reachability for LTI Systems with Two-Level Lattice Neural Network Controllers
James Ferlez, Yasser Shoukry
In this paper, we consider the computational complexity of bounding the reachable set of a Linear Time-Invariant (LTI) system controlled by a Rectified Linear Unit (ReLU) Two-Level…
CertiFair: A Framework for Certified Global Fairness of Neural Networks
Haitham Khedr, Yasser Shoukry
We consider the problem of whether a Neural Network (NN) model satisfies global individual fairness. Individual Fairness suggests that similar individuals with respect to a certain…
PolyARBerNN: A Neural Network Guided Solver and Optimizer for Bounded Polynomial Inequalities
Wael Fatnassi, Yasser shoukry
Constraints solvers play a significant role in the analysis, synthesis, and formal verification of complex embedded and cyber-physical systems. In this paper, we study the problem…
NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing
Ulices Santa Cruz, Yasser Shoukry
In this paper, we consider the problem of formally verifying a Neural Network (NN) based autonomous landing system. In such a system, a NN controller processes images from a camera…
VindiCo: Privacy Safeguard Against Adaptation Based Spyware in Human-in-the-Loop IoT
Salma Elmalaki, Bo-Jhang Ho, Moustafa Alzantot +2
Personalized IoT adapts their behavior based on contextual information, such as user behavior and location. Unfortunately, the fact that personalized IoT adapts to user context ope…
Fast BATLLNN: Fast Box Analysis of Two-Level Lattice Neural Networks
James Ferlez, Haitham Khedr, Yasser Shoukry
In this paper, we present the tool Fast Box Analysis of Two-Level Lattice Neural Networks (Fast BATLLNN) as a fast verifier of box-like output constraints for Two-Level Lattice (TL…
NNSynth: Neural Network Guided Abstraction-Based Controller Synthesis for Stochastic Systems
Xiaowu Sun, Yasser Shoukry
In this paper, we introduce NNSynth, a new framework that uses machine learning techniques to guide the design of abstraction-based controllers with correctness guarantees. NNSynth…
Assured Neural Network Architectures for Control and Identification of Nonlinear Systems
James Ferlez, Yasser Shoukry
In this paper, we consider the problem of automatically designing a Rectified Linear Unit (ReLU) Neural Network (NN) architecture (number of layers and number of neurons per layer)…
Provably Safe Model-Based Meta Reinforcement Learning: An Abstraction-Based Approach
Xiaowu Sun, Wael Fatnassi, Ulices Santa Cruz +1
While conventional reinforcement learning focuses on designing agents that can perform one task, meta-learning aims, instead, to solve the problem of designing agents that can gene…
Safe-by-Repair: A Convex Optimization Approach for Repairing Unsafe Two-Level Lattice Neural Network Controllers
Ulices Santa Cruz, James Ferlez, Yasser Shoukry
In this paper, we consider the problem of repairing a data-trained Rectified Linear Unit (ReLU) Neural Network (NN) controller for a discrete-time, input-affine system. That is we…
Provably Correct Training of Neural Network Controllers Using Reachability Analysis
Xiaowu Sun, Yasser Shoukry
In this paper, we consider the problem of training neural network (NN) controllers for nonlinear dynamical systems that are guaranteed to satisfy safety and liveness (e.g., reach-a…
PolyAR: A Highly Parallelizable Solver For Polynomial Inequality Constraints Using Convex Abstraction Refinement
Wael Fatnassi, Yasser Shoukry
Numerical tools for constraints solving are a cornerstone to control verification problems. This is evident by the plethora of research that uses tools like linear and convex progr…
Bounding the Complexity of Formally Verifying Neural Networks: A Geometric Approach
James Ferlez, Yasser Shoukry
In this paper, we consider the computational complexity of formally verifying the behavior of Rectified Linear Unit (ReLU) Neural Networks (NNs), where verification entails determi…
PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier
Haitham Khedr, James Ferlez, Yasser Shoukry
Neural Networks (NNs) have increasingly apparent safety implications commensurate with their proliferation in real-world applications: both unanticipated as well as adversarial mis…
ShieldNN: A Provably Safe NN Filter for Unsafe NN Controllers
James Ferlez, Mahmoud Elnaggar, Yasser Shoukry +1
In this paper, we develop a novel closed-form Control Barrier Function (CBF) and associated controller shield for the Kinematic Bicycle Model (KBM) with respect to obstacle avoidan…
Two-Level Lattice Neural Network Architectures for Control of Nonlinear Systems
James Ferlez, Xiaowu Sun, Yasser Shoukry
In this paper, we consider the problem of automatically designing a Rectified Linear Unit (ReLU) Neural Network (NN) architecture (number of layers and number of neurons per layer)…