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!

Tools I lead

IMPaCT reach-while-avoid result: a stochastic trajectory in the x1-x2 state space skirting the red avoid region and reaching the green target set

IMPaCT: Interval MDP Parallel Construction for Controller Synthesis of Large-Scale Stochastic Systems

PRoTECT jet-engine case study: barrier-certificate level sets separating trajectories starting in the initial set from the unsafe region

PRoTECT: Parallelized Construction of Safety Barrier Certificates for Nonlinear Polynomial Systems

Scen-Opt web app: the linear-program tab showing a robust scenario formulation with editable constraint matrices and solver options

Scen-Opt: A Scenario Optimization Toolbox for Data-Driven Convex Programming

TRUST predator-prey case study: closed system trajectories enclosed by barrier level sets that separate them from the unsafe regions in the four corners

TRUST: Stability and Safety Controller Synthesis for Unknown Dynamical Models Using a Single Trajectory

Tools I contribute to

BehaVerify pipeline: behavior-tree DSL, ONNX and nuXmv inputs feed a parser and model builder, whose code generators emit SMV, Python, C++, Haskell, LaTeX and runtime-monitor artefacts for model checking, simulation and on-robot monitoring

BehaVerify: A Formal Verification Tool for Behavior Trees

n2v architecture: ONNX networks and VNN-LIB specifications parsed into reachability solvers feeding verifier and falsifier frontends

n2v: Neural Network Verification in Python

NNV reachability analysis: reachable set of a neural-network controlled system spiralling inside its safe set

NNV: Neural Network Verification Toolbox for MATLAB