The ALC Design Studio enables an engineer to design Cyber-Physical Systems (CPS's) with integrated learning-enabled components (LECs).

Domain specific embedded stream language for generating hard real-time C code for monitors.

Control Systems Analysis Framework (CSAF) is a framework to minimize the effort required to evaluate, implement, and verify controller design (classical and learning enabled) with respect to the system dynamics.

A software toolkit for the formal design and analysis of systems that include VerifAI: artificial intelligence (AI) and machine learning (ML) components.

A hybrid system theorem prover that can analyze safety properties of a control program or learned policy in a physical model by combining offline proofs with verified runtime monitoring by ModelPlex.

A framework for verifying deep neural networks. It can answer queries about a network's properties by transforming them into constraint satisfaction problems, accommodate networks with different activation functions and topologies, and perform high-level reasoning on the network to reduce search space and improve performance.

Exploration tool for Neural Network Verification (NNV) tool from Verivital Labs, Vanderbilt University.

A domain-specific probabilistic programming language for modeling the environments of cyber-physical systems like robots and autonomous cars.

Integrates Overt and MIPVerify tools for the purpose of verifying closed-loop systems that are controlled by neural networks.

Integrates the ModelPlex monitor and reachability analysis for monitoring a reinforcement-learning-based Dubins path following controller and recovering from unsafe control.

A state-of-the-art sound and complete verification toolkit for Relu-based feed-forward neural networks.

A tool for verifying safety properties of closed-loop systems with neural network components.

A domain-specific probabilistic programming language for modeling the environments of cyber-physical systems like robots and autonomous cars.

A tool to quantify uncertainty in machine learning models using predictive coding.

Architecture and Analysis for High-Assurance Autonomy.

ReSonAte is a mehodology that estimates the dynamic risk of Autonomous Cyber-Physical Systems.

Supports the development and management of safety/assurance cases.

A simple, generic and fast implementation of Deepmind's AlphaZero algorithm.

Data-driven, on-the-fly control of systems with unknown dynamics.

A Fisher informed trust-region method for training Deep Neural Networks using higher order optimization techniques.

A framework for navigation around humans combining learning-based perception with model-based optimal control.

Approach is based on the premise that patterns in a large input data space can be effectively captured in a smaller manifold space, from which similar yet novel test cases---both the input and the label---can be sampled and generated.

Imitation-Projected Programmatic Reinforcement Learning.

Robustness to Adversarial Attacks in Learning-Enabled Controllers. Finds adversarial attacks and synthesizes shields to defend the system against them.

A tool for verified training in reinforcement learning. Revel offers guaranteed safety at training time using an iteratively updated shield to bound the behavior of the learner.

Recurrent network implicit distributions for anomaly detection in dynamic processes.