Software Tools
Presented below is a collection of the software tools I have created or contributed to as part of my research. Do check them out!
IMPaCT: Interval MDP Parallel Construction for Controller Synthesis of Large-Scale Stochastic Systems
IMPaCT is an open-source software tool for the parallelised verification and controller synthesis of large-scale stochastic systems using interval Markov chains (IMCs) and interval Markov decision processes (IMDPs), respectively. The tool serves to (i) construct IMCs/IMDPs as finite abstractions of underlying original systems, and (ii) leverage interval iteration algorithms for formal verification and controller synthesis over infinite-horizon properties, including safety, reachability, and reach-while-avoid, while offering convergence guarantees.
PRoTECT: Parallelized Construction of Safety Barrier Certificates for Nonlinear Polynomial Systems
PRoTECT is an open-source software tool for the parallelized construction of safety barrier certificates (BCs) for nonlinear polynomial systems. This tool employs sum-of-squares (SOS) optimization programs to systematically search for polynomial-type BCs, while aiming to verify safety properties over four classes of dynamical systems: (i) discrete-time stochastic systems, (ii) discrete-time deterministic systems, (iii) continuous-time stochastic systems, and (iv) continuous-time deterministic systems.
TRUST: Stability and Safety Controller Synthesis for Unknown Dynamical Models Using a Single Trajectory
TRUST is an open-source software tool developed for data-driven controller synthesis of dynamical systems with unknown mathematical models, ensuring either stability or safety properties. By collecting only a single input-state trajectory from the unknown system and satisfying a rank condition that ensures the system is persistently excited according to the Willems et al.'s fundamental lemma, TRUST aims to design either control Lyapunov functions (CLF) or control barrier certificates (CBC), along with their corresponding stability or safety controllers.
NNV: Neural Network Verification Toolbox for MATLAB
NNV is an open-source MATLAB toolbox for the formal verification of deep neural networks and learning-enabled cyber-physical systems, developed by the VeriVITAL research group at Vanderbilt University. It implements set-based reachability analysis using star sets and their extensions, supporting feedforward, convolutional, recurrent, and graph networks, neural ODEs, and neural network control systems. I am a contributor to NNV3.
n2v: Neural Network Verification in Python
n2v is a Python translation of the NNV toolbox. It verifies properties of neural networks using sound set-based reachability analysis and probabilistic verification via conformal inference, with support for PyTorch models and ONNX networks.