I currently contribute or have contributed to the following toolboxes.


BluSTL (pronounced "blue steel") is a MATLAB toolkit for automatically generating hybrid controllers from specifications written in Signal Temporal Logic.

Diagnosis and Repair for sYnthesis (DiaRY)

This MATLAB package contains the implementation of the algorithms described in the paper "Diagnosis and Repair for Synthesis from Signal Temporal Logic", Ghosh et al, HSCC 2016. This file describes the contents of the package, and provides instruction regarding its use.

Linear Temporal Logic MissiOn Planner (LTLMoP)

LTLMoP is a modular Python toolkit for designing, testing, and implementing hybrid controllers generated automatically from task specifications written in Structured English, Temporal Logic or a subset of Natural Language.

SmalL bUt Complete GROne Synthesizer (slugs)

slugs is a stand-alone reactive synthesis tool for generalized reactivity(1) synthesis.

The Temporal Logic Planning Toolbox (TuLiP)

TuLiP is a collection of Python code for automatic synthesis of correct-by-construction embedded control software.