In the lists below, we summarize the current actively maintained tools for the analysis and synthesis of hybrid systems. The lists are compiled by Prof. Dr. Manuel Mazo and Mr. Mahmoud Khaled. Modeling and Identification (Languages and Tools): Tool Description Link Last Maintained SARXSAT SARXSAT is a tool for the identification of Switched and Piece-wise ARX models employing sparsification via l_0 minimization and SAT solvers. open 10.2019 Ptolemy II Ptolemy II is an open-source software framework supporting experimentation with actor-oriented design. open 06.2018 LUSTRE LUSTRE is a data flow synchronous language, designed for programming reactive system. Tools like SCADE use LUSTRE. open N/A MODEST The Modest toolset supports the modelling and analysis of hybrid, real-time, distributed and stochastic systems. open 09.2019 HyLink HyLink is a tool which links Simulink/Stateflow models(SLSF) to the world of hybrid automaton. open 08.2012 CHARON CHARON is a language for modular specification of interacting hybrid systems based on the notions of agent and mode. open N/A IOA IOA is a formal language for describing computational processes that are modeled using I/O automata. open 08.2003 Möbius Möbius™ is a software tool for modeling the behavior of complex systems. open 12.2018 SIGNAL SIGNAL is a programming language based on synchronized data-flow (flows + synchronization): a process is a set of equations on elementary flows describing both data and control. open N/A HyEQ A Hybrid Systems Simulation Toolbox for Matlab/Simulink open 05/2017 Verification of Hybrid Systems: Tool Description Link Last Maintained Evrostos Evrostos is the first tool for model checking formulas in Robust Linear Temporal Logic (rLTL). open 12.2020 JuliaReach JuliaReach is a toolbox for set-based reachability analysis of dynamical systems. open 12.2020 PIRK PIRK is a tool to efficiently compute reachable sets for general nonlinear systems of extremely high dimensions. It introduces three parallel algorithms for computing interval approximations of forward reachable sets. open 02.2020 SReachTools SReachTools is an open-source MATLAB toolbox for performing stochastic reachability of linear, potentially time-varying, discrete-time systems that are perturbed by a stochastic disturbance. open 05.2020 TIRA TIRA is a Matlab library gathering several methods for the computation of interval over-approximations of the reachable sets for both continuous- and discrete-time nonlinear systems. open 12.2019 AVERIST AVERIST implements an algorithmic approach for the stability analysis of polyhedral switched systems. open 03.2015 DSValidator DSValidator is an automated counterexample reproducibility tool based on MATLAB, with the goal of reproducing counterexamples that refute specific properties related to digital systems. open 07.2017 HyLAA Hylaa (HYbrid Linear Automata Analyzer) is a verification tool for system models with linear ODEs, time-varying inputs, and possibly hybrid dynamics. open 10.2019 STORM Storm is a tool for the analysis of systems involving random or probabilistic phenomena. open 06.2020 xSAP xSAP is a tool for safety assessment of synchronous finite-state and infinite-state systems. It is based on symbolic model checking techniques. open 03.2016 Axelerator Axelerator is a tool for reachability analysis of open guarded linear time Invariant systems through the use of abstract acceleration. The tool allows the evaluation of reach tubes for both finite and infinite time horizons. open 06.2019 C2E2 C2E2 is a tool for verifying hybrid automata. C2E2 can automatically check bounded time invariant properties of nonlinear hybrid automata. open 11.2018 dReach dReach is a bounded reachability analysis tool for nonlinear hybrid systems. open 12.2020 Flow* Flow*: an analyzer for non-linear hybrid systems. It performs Taylor model-based flowpipe construction for non-linear (polynomial) hybrid systems. open 03.2017 HyComp HyComp is a model checker for hybrid systems based on satisfiability modulo theories (SMT). open 10.2014 ProbReach ProbReach is collection of tools for calculating probability of bounded reachability in hybrid systems with parametric uncertainties. open 11.2019 CoVerTS CoVerTS is a tool for the verification of state properties for timed systems. it served as a proof of concept for "Compositional Invariant Generation for Timed Systems". open 12.2014 JSR JSR is a toolbox for computing the Joint Spectral Radius of a set of matrices, i.e., the maximal asymptotic growth rate of products of matrices taken in that set. open 03.2016 VeriSiMPL This toolbox is used to generate finite abstractions of autonomous Max-Plus-Linear (MPL) systems over R^n. open 12.2016 HyCreate HyCreate is a software tool for defining hybrid automata and computing over-approximations of reachable sets for systems with nonlinear, nondeterministic dynamics with a small number of dimensions. open 03.2018 OCRA OCRA is a command-line tool for the verification of logic-based contract refinement for embedded systems. open 07.2020 Stabhyli Stabhyli is a tool that automatically proves stability (global asymptotic stability) of non-linear hybrid systems. The tool was created in the context of AVACS H4. open 11.2015 BigMC BigMC (Bigraphical Model Checker) is a model-checker designed to operate on Biographical Reactive Systems (BRS). open 08.2012 CORA The COntinuous Reachability Analyzer (CORA) is a collection of MATLAB classes for the formal verification of cyber-physical systems using reachability analysis. open 11.2018 HYMITATOR HYMITATOR is a tool dedicated to the synthesis of parameters for hybrid automata (HA). It is a fork of IMITATOR, the tool for parameter synthesis in timed automata. open 04.2012 Passel Passel is a software tool for analyzing networked hybrid models with arbitrarily many components. Passel is now integrated as a module in HyST (see details below). open 04.2014 PyPPL The Parma Polyhedra Library (PPL) provides numerical abstractions especially targeted at applications in the field of analysis and verification of complex systems. open 02.2016 opaal opaal is a distributed/parallel (discrete time) model checker for networks of timed automata implemented in Python using MPI. open 11.2016 SpaceEx The SpaceEx tool platform is designed to facilitate the implementation of algorithms related to reachability and safety verification. open 02.2015 CARTS CARTS (Compositional Analysis of Real-Time Systems) is developed as a platform-independent tool that automatically generates resource interfaces needed for the compositional analysis of real-time systems. open 06.2018 JTLV JTLV is a tool aimed to facilitate and provide a unified framework to the development of formal verification algorithms. open 03.2008 PASS PASS is an analysis tool for infinite-state probabilistic models. It is based on predicate abstraction and automatic abstraction refinement. open 07.2012 INFAMY INFAMY is a tool with the purpose of model checking CSL formulae on infinite state Markov chains in continuous time, specified in a variant of the PRISMlanguage. open 12.2009 Roméo Roméo is a software studio for Time Petri Net analysis, developed in the Real-Time Systems Team at IRCCyN . It performs analysis on T-Time Petri nets and on one of their extension to scheduling. open 11.2020 BACH BACH stands for Bounded reAcheability CHecker, it is a bounded model checker for Linear Hybrid Systems. BACH was designed and implemented by Software Engineering Group, Nanjing University. open 05.2017 KeYmaera X KeYmaera is A hybrid theorem prover for hybrid systems. KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. open 12.2020 MLSolver A tool for solving the satisfiability and validity problems for modal fixpoint logics. open 12.2016 HSolver HSolver is a program for verification of hybrid systems based on the constraint solver RSOLVER. Unlike other packages its correctness does not depend on floating point rounding errors. It can handle non-linear ordinary differential equations, but is not optimized for simpler continuous dynamics. open 11.2007 SAAtRe AAtRe is an abstraction refinement model checker for timed automata based on extended SAT-solving techniques. open 10.2012 MATISSE MATISSE is a free MATLAB toolbox for safety verification and reachable set computation of large dimensional, constrained linear systems. open 07.2005 PHAVer PHAVer is a new tool for the exact verification of safety properties of hybrid systems with piecewise constant bounds on the derivatives. open 02.2007 Hybrid Toolbox for MATLAB The Hybrid Toolbox is a MATLAB/Simulink toolbox for modeling, simulating, and verifying hybrid dynamical systems, for designing and simulating model predictive controllers for hybrid systems subject to constraints, and for generating linear and hybrid MPC control laws in piecewise affine form that can be directly embedded as C-code in real-time applications. open 11.2020 PRISM 2 PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour. open 04.2020 Polychrony Polychrony is an integrated development environment and technology demonstrator. open 05.2010 Sigali Sigali is a model-checking tool-based which manipulates ILTS: Implicit Labeled Transition Systems (which can be seen as an equational representation of an automaton) as intermediate models for discrete event systems. open 06.2007 NBAC NBAC analyses synchronous and deterministic reactive systems containing combination of Boolean and numerical variables and continuously interacting with an external environment. open 02.2011 HyTech HyTech is an automatic tool for the analysis of embedded systems. HyTech computes the condition under which a linear hybrid system satisfies a temporal requirement. open 06.2002 UPPAAL Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.). open 11.2019 LRT-NG LRT-NG is a toolset that computes a reachtube (an over-approximation of the set of reachable states over a given time horizon) of continuous-depth neural networks as well as any other nonlinear dynamical systems. open 12.2021 GoTube GoTube constructs stochastic reachtubes (= the set of all reachable system states) of continuous-time systems. GoTube is made deliberately for the verification of countinuous-depth neural networks. open 12.2021 Controller Synthesis for Hybrid Systems: Tool Description Link Last Maintained OmegaThreads OmegaThreads is a tool for parallel automated controller synthesis for dynamical systems to satisfy ω-regular specifications given as LTL formulae. open 12.2020 pFaces pFaces is an the acceleration ecosystem for formal methods. open 10.2020 StocHy StocHy simplifies both the modelling and design of stochastic hybrid systems (SHS) and their analysis. open 12.2019 BoSy BoSy is a synthesis tool based on a various bounded synthesis encodings. open 12.2017 ROCS ROCS is an algorithmic control synthesis tool for nonlinear dynamical systems. open 12.2020 SafetySynth SafetySynth is a tool for synthesizing controllers from safety benchmarks given in the SyntComp AIGER format. open 12.2016 AMYTISS AMYTISS builds finite Markov decision processes (MDPs) as finite abstractions from stochastic discrete-time systems and synthesizes controllers for them satisfying bounded-time safety specifications and reach-avoid specifications. open 06.2020 SENSE SENSE is a tool for the automatic controller synthesis of complex plants in the networked control systems (NCS) based on symbolic models. open 12.2018 DSSynth DSSynth synthesizes sound digital controllers for physical plants that are represented as linear time-invariant systems with single input and output. open 12.2019 QUEST QUEST is a tool for automated controller synthesis for incrementally input-to-state stable nonlinear control systems with respect to safety and reachability specifications. open 12.2017 Sapo Sapo is a tool for the formal analysis of polynomial dynamical systems. Its main features are reachability computation and parameter synthesis. open 12.2016 SCOTS SCOTS is a tool for the automatic controller synthesis of nonlinear control systems based on symbolic models. A ready/easy to install version is also available here. open 12.2019 slugs Slugs is a stand-alone reactive synthesis tool for generalized reactivity(1) synthesis. It uses binary decision diagrams (BDDs) as the primary data structure for efficient symbolic reasoning. open 01.2020 BluSTL BluSTL (pronounced "blue steel") is a MATLAB toolkit for automatically generating hybrid controllers from specifications written in Signal Temporal Logic. open 12.2014 Demiurge Demiurge is a tool to synthesize a correct-by-construction implementation of a reactive system from a declarative safety specification. open 12.2015 FAUST 2 FAUST2 is a software tool that generates abstractions of (possibly non-deterministic) discrete-time Markov processes (dtMP) defined over uncountable (continuous) state spaces. open 02.2014 reasyns Reasyns generates a library of atomic controllers for nonlinear systems satisfying a high-level controller (a finite state machine) synthesized from a reactive mission specification. open 12.2016 AbsSynthe Swiss AbsSynthe - is the native version of the AbsSynthe tool, used to synthesize controllers from succinct safety specifications. open 03.2020 CoSyMA CoSyMA is a tool for automatic controller synthesis for incrementally stable switched systems based on multi-scale discrete abstractions. open 11.2017 LtlOpt LtlOpt is a Matlab tool for the optimal control of high-dimensional, nonlinear robotic systems with linear temporal logic (LTL) specifications. open 08.2014 gr1c gr1c is a collection of tools for GR(1) synthesis and related activities. Its core functionality is checking realizability of and synthesizing strategies for GR(1) specifications, though it does much more. open 02.2020 Pessoa 2.0 Pessoa is a tool for the synthesis of correct-by-design embedded control software. open 06.2011 TuLiP TuLiP is a tool for automatic synthesis of correct-by-construction embedded control software. open 11.2016 ARCS ARCS is a toolbox for abstraction-refinement-based incremental synthesis of correct-by-construction switching protocols. open 12.2018 Mascot Mascot is a tool for synthesizing controllers for continuous non-linear dynamical systems. open 12.2018 Synthia Synthia is a tool for the verification and synthesis of open real-time systems modeled as timed automata. open 12.2011 TALIRO-TOOLS TALIRO (TemporAl LogIc RObustness) tools is a suit of tools for the analysis of continuous and hybrid dynamical systems using linear time temporal logics. open 10.2019 Quasy Quasy is a tool for synthesis of reactive systems which takes qualitative and quantitative specifications in GOAL format. open 07.2011 Unbeast Unbeast is a tool capable of handling full linear-time temporal logic (LTL). It is designed for specifications comprising a set of assumptions and a set of guarantees. open 11.2012 LTLMoP The LTLMoP (Linear Temporal Logic MissiOn Planning) toolkit is a collection of Python applications for designing, testing, and implementing hybrid controllers generated automatically from task specifications written in Structured English or Temporal Logic. open 12.2015 ALPAGA Alpaga is a software tool computing strategies for imperfect information parity games, using antichains during the computations to gain efficiency. open 12.2009 dtControl Decision tree learning algorithms for controller representation open 12.2021 AROC A Toolbox for Automated Reachset Optimal Controller open 12.2021 FOSSIL A Software Tool for the Formal Synthesis of Lyapunov Functions and Barrier Certificates using Neural Networks open 12.2021 Other tools: Tool Description Link Last Maintained BDD2Implement BDD2Implement is a tool to generate hardware/software implementations of BDD-based symbolic controllers. The implementations come in form of source-code (VHDL/Verilog for FPGAs and C/C++ for other systems). open 10.2020 COTONN COTONN is a a tool for converting symbolic controllers (from SCOTS) into neural network representation. open 12.2018 SCOTS2FPGA SCOTS2FPGA provides space efficient implementations of symbolic controllers on FPGAs. open 06.2019 HYST HYST is a HYbrid Source Transformer. HYST is a source-to-source translation tool, currently taking input in the SpaceEx model format, and translating to the formats of HyCreate, Flow*, or dReach. open 04.2015 SL2SX SL2SX is a tool that translates Simulink models (saved in XML format) into SpaceEx models (respecting the SX format). open 12.2017
