65 citations · 306 across the 20 of their papers we have counts for
21 papers
Reachability Analysis for Linear Systems with Uncertain Parameters using Polynomial Zonotopes
Yushen Huang, Ertai Luo, Stanley Bak +1
In real world applications, uncertain parameters are the rule rather than the exception. We present a reachability algorithm for linear systems with uncertain parameters and inputs…
Fully Automated Verification of Linear Time-Invariant Systems against Signal Temporal Logic Specifications via Reachability Analysis
Niklas Kochdumper, Stanley Bak
While reachability analysis is one of the most promising approaches for formal verification of dynamic systems, a major disadvantage preventing a more widespread application is the…
On the Difficulty of Intersection Checking with Polynomial Zonotopes
Yushen Huang, Ertai Luo, Stanley Bak +1
Polynomial zonotopes, a non-convex set representation, have a wide range of applications from real-time motion planning and control in robotics, to reachability analysis of nonline…
First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)
Christopher Brix, Mark Niklas Müller, Stanley Bak +2
This paper presents a summary and meta-analysis of the first three iterations of the annual International Verification of Neural Networks Competition (VNN-COMP) held in 2020, 2021,…
Provable Fairness for Neural Network Models using Formal Verification
Giorgian Borca-Tasciuc, Xingzhi Guo, Stanley Bak +1
Machine learning models are increasingly deployed for critical decision-making tasks, making it important to verify that they do not contain gender or racial biases picked up from…
Provably Safe Reinforcement Learning via Action Projection using Reachability Analysis and Polynomial Zonotopes
Niklas Kochdumper, Hanna Krasowski, Xiao Wang +2
While reinforcement learning produces very promising results for many applications, its main disadvantage is the lack of safety guarantees, which prevents its use in safety-critica…
Fully-Automated Verification of Linear Systems Using Inner- and Outer-Approximations of Reachable Sets
Mark Wetzlinger, Niklas Kochdumper, Stanley Bak +1
Reachability analysis is a formal method to guarantee safety of dynamical systems under the influence of uncertainties. A substantial bottleneck of all reachability algorithms is t…
Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes
Niklas Kochdumper, Christian Schilling, Matthias Althoff +1
We present a novel approach to efficiently compute tight non-convex enclosures of the image through neural networks with ReLU, sigmoid, or hyperbolic tangent activation functions.…
Neural Network Compression of ACAS Xu Early Prototype is Unsafe: Closed-Loop Verification through Quantized State Backreachability
Stanley Bak, Hoang-Dung Tran
ACAS Xu is an air-to-air collision avoidance system designed for unmanned aircraft that issues horizontal turn advisories to avoid an intruder aircraft. Due the use of a large look…
Stress Testing Autonomous Racing Overtake Maneuvers with RRT
Stanley Bak, Johannes Betz, Abhinav Chawla +2
High-performance autonomy often must operate at the boundaries of safety. When external agents are present in a system, the process of ensuring safety without sacrificing performan…
The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results
Stanley Bak, Changliu Liu, Taylor Johnson
This report summarizes the second International Verification of Neural Networks Competition (VNN-COMP 2021), held as a part of the 4th Workshop on Formal Methods for ML-Enabled Aut…
Reachability of Black-Box Nonlinear Systems after Koopman Operator Linearization
Stanley Bak, Sergiy Bogomolov, Parasara Sridhar Duggirala +2
Reachability analysis of nonlinear dynamical systems is a challenging and computationally expensive task. Computing the reachable states for linear systems, in contrast, can often…
Automatic Dynamic Parallelotope Bundles for Reachability Analysis of Nonlinear Systems
Edward Kim, Stanley Bak, Parasara Sridhar Duggirala
Reachable set computation is an important technique for the verification of safety properties of dynamical systems. In this paper, we investigate reachable set computation for disc…
The Black-Box Simplex Architecture for Runtime Assurance of Autonomous CPS
Usama Mehmood, Sanaz Sheikhi, Stanley Bak +2
The Simplex Architecture is a runtime assurance framework where control authority may switch from an unverified and potentially unsafe advanced controller to a backup baseline cont…
Verification of Deep Convolutional Neural Networks Using ImageStars
Hoang-Dung Tran, Stanley Bak, Weiming Xiang +1
Convolutional Neural Networks (CNN) have redefined the state-of-the-art in many real-world applications, such as facial recognition, image classification, human pose estimation, an…
NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems
Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez +5
This paper presents the Neural Network Verification (NNV) software tool, a set-based verification framework for deep neural networks (DNNs) and learning-enabled cyber-physical syst…
Efficient n-to-n Collision Detection for Space Debris using 4D AABB Trees (Extended Report)
Stanley Bak, Kerianne Hobbs
Collision detection algorithms are used in aerospace, swarm robotics, automotive, video gaming, dynamics simulation and other domains. As many applications of collision detection r…
Cyber-Physical Specification Mismatches
Luan V. Nguyen, Khaza Anuarul Hoque, Stanley Bak +2
Embedded systems use increasingly complex software and are evolving into cyber-physical systems (CPS) with sophisticated interaction and coupling between physical and computational…
Numerical Verification of Affine Systems with up to a Billion Dimensions
Stanley Bak, Hoang-Dung Tran, Taylor T. Johnson
Affine systems reachability is the basis of many verification methods. With further computation, methods exist to reason about richer models with inputs, nonlinear differential equ…
A Comparison of Approaches for Solving Hard Graph-Theoretic Problems
Victoria Horan, Steve Adachi, Stanley Bak
In order to formulate mathematical conjectures likely to be true, a number of base cases must be determined. However, many combinatorial problems are NP-hard and the computational…
S3A: Secure System Simplex Architecture for Enhanced Security of Cyber-Physical Systems
Sibin Mohan, Stanley Bak, Emiliano Betti +3
Until recently, cyber-physical systems, especially those with safety-critical properties that manage critical infrastructure (e.g. power generation plants, water treatment faciliti…