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. A set of related tools for Discrete Event Systems (with some overlap to the ones here) can be found at: https://ieeecss.org/tc/discrete-event-systems/resources Modeling and Identification (Languages and Tools): Tool Description Link Last Maintained CHARON CHARON is a language for modular specification of interacting hybrid systems based on the notions of agent and mode. open N/A CyPhyHouse and Koord Language Framework for programming, simulating, and deploying multi-robot systems. open 12.2020 HIT Hybrid Systems Identification Toolbox open 04.2023 HyEQ A Hybrid Systems Simulation Toolbox for Matlab/Simulink open 10.2022 HyLink HyLink is a tool which links Simulink/Stateflow models(SLSF) to the world of hybrid automaton. open 08.2012 HySynth Synthesis of hybrid automata from time-series data open 04.2023 IOA IOA is a formal language for describing computational processes that are modeled using I/O automata. open 08.2003 LUSTRE LUSTRE is a data flow synchronous language, designed for programming reactive system. Tools like SCADE use LUSTRE. open N/A Möbius Möbius™ is a software tool for modeling the behavior of complex systems. open 12.2018 MODEST The Modest toolset supports the modelling and analysis of hybrid, real-time, distributed and stochastic systems. open 09.2019 Pacti Description: Open-source Python package for compositional system analysis and design using assume-guarantee specifications, or contracts. open 09.2023 Ptolemy II Ptolemy II is an open-source software framework supporting experimentation with actor-oriented design. open 06.2018 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 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 Zélus Zélus is a synchronous language extended with Ordinary Differential Equations (ODEs) to program hybrid systems that mix discrete-time and continuous-time models. open 06.2023 Verification of Hybrid Systems: Tool Description Link Last Maintained Ariadne C++/Python library for formal verification of cyber-physical systems, using reachability analysis and rigorous numerics on nonlinear hybrid automata open 04.2023 AVERIST AVERIST implements an algorithmic approach for the stability analysis of polyhedral switched systems. open 03.2015 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 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 BigMC BigMC (Bigraphical Model Checker) is a model-checker designed to operate on Biographical Reactive Systems (BRS). open 08.2012 C2E2 C2E2 is a tool for verifying hybrid automata. C2E2 can automatically check bounded time invariant properties of nonlinear hybrid automata. open 11.2018 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 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.2022 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 dReach dReach is a bounded reachability analysis tool for nonlinear hybrid systems. open 12.2020 DryVR Verification tool for hybrid models with black-box dynamics. open 06.2022 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 Evrostos Evrostos is the first tool for model checking formulas in Robust Linear Temporal Logic (rLTL). 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 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 HooVer Statistical model checking of black box models using optimistic optimization. open 05.2023 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 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 HyComp HyComp is a model checker for hybrid systems based on satisfiability modulo theories (SMT). open 10.2014 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 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 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 HyPro HyPro is a c++ programming library for the development of hybrid systems analysis tools. The library is built around a collection of commonly used state set representations for flowpipe construction-based reachability analysis of linear hybrid systems but has been extended towards rectangular, singular and timed systems. open 11.2021 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 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 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 JTLV JTLV is a tool aimed to facilitate and provide a unified framework to the development of formal verification algorithms. open 03.2008 JuliaReach JuliaReach is a toolbox for set-based reachability analysis of dynamical systems. open 12.2020 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 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 MATISSE MATISSE is a free MATLAB toolbox for safety verification and reachable set computation of large dimensional, constrained linear systems. open 07.2005 MLSolver A tool for solving the satisfiability and validity problems for modal fixpoint logics. open 12.2016 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 OCRA OCRA is a command-line tool for the verification of logic-based contract refinement for embedded systems. open 07.2020 opaal opaal is a distributed/parallel (discrete time) model checker for networks of timed automata implemented in Python using MPI. open 11.2016 PASS PASS is an analysis tool for infinite-state probabilistic models. It is based on predicate abstraction and automatic abstraction refinement. open 07.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 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 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 Polychrony Polychrony is an integrated development environment and technology demonstrator. open 05.2010 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 ProbReach ProbReach is collection of tools for calculating probability of bounded reachability in hybrid systems with parametric uncertainties. open 11.2019 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 R2U2 (Realizable Responsive Unobtrusive Unit) Flight-certifiable, real-time, stream-based, online, embedded runtime verification engine with provable bounds on size (in hardware/FPGA or software), and unobtrusiveness. There are 3 implementations (FGPA, C, C++), and R2U2 runs stand-alone (without system instrumentation), interacting via message-passing. The input language includes both future-time and past-time temporal logics. open 06.2023 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 SAAtRe AAtRe is an abstraction refinement model checker for timed automata based on extended SAT-solving techniques. open 10.2012 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 SpaceEx The SpaceEx tool platform is designed to facilitate the implementation of algorithms related to reachability and safety verification. open 02.2015 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 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 STORM Storm is a tool for the analysis of systems involving random or probabilistic phenomena. open 06.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 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 VeriSiMPL This toolbox is used to generate finite abstractions of autonomous Max-Plus-Linear (MPL) systems over R^n. open 12.2016 Verse Python library for modeling, simulating, and verifying multi-agent hybrid scenario with support for new algorithm development. open 06.2023 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 Controller Synthesis for Hybrid Systems: Tool Description Link Last Maintained AbsSynthe Swiss AbsSynthe - is the native version of the AbsSynthe tool, used to synthesize controllers from succinct safety specifications. open 03.2020 ALPAGA Alpaga is a software tool computing strategies for imperfect information parity games, using antichains during the computations to gain efficiency. open 12.2009 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 ARCS ARCS is a toolbox for abstraction-refinement-based incremental synthesis of correct-by-construction switching protocols. open 12.2018 AROC A Toolbox for Automated Reachset Optimal Controller open 12.2021 BluSTL BluSTL (pronounced "blue steel") is a MATLAB toolkit for automatically generating hybrid controllers from specifications written in Signal Temporal Logic. open 12.2014 BoSy BoSy is a synthesis tool based on a various bounded synthesis encodings. open 12.2017 CoSyMA CoSyMA is a tool for automatic controller synthesis for incrementally stable switched systems based on multi-scale discrete abstractions. open 11.2017 Demiurge Demiurge is a tool to synthesize a correct-by-construction implementation of a reactive system from a declarative safety specification. open 12.2015 Dionysos Open-source software for the analysis and control of hybrid systems via smart symbolic models. open 02.2024 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 dtControl Decision tree learning algorithms for controller representation open 12.2021 ETCetera Toolchain for the Scheduling of Event-Triggered Controllers open 07.2022 FACTEST Guaranteed model-based controller synthesis for reach-avoid problems. open 12.2020 Fairsyn A solver for two-player games, two-player fair adversarial games, and turn-based stochastic games on finite game arenas. open 05.2023 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 FOSSIL A Software Tool for the Formal Synthesis of Lyapunov Functions and Barrier Certificates using Neural Networks open 12.2021 Genie A flexible abstract solver for Rabin games using optimized symbolic fixpoint algorithm. open 05.2023 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 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 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 Mascot Mascot is a tool for synthesizing controllers for continuous non-linear dynamical systems. open 12.2018 Mascot-SDS Abstraction-based control of stochastic dynamical systems with omega-regular control objectives. open 05.2023 OmegaThreads OmegaThreads is a tool for parallel automated controller synthesis for dynamical systems to satisfy ω-regular specifications given as LTL formulae. open 12.2020 Pessoa 2.0 Pessoa is a tool for the synthesis of correct-by-design embedded control software. open 06.2011 pFaces pFaces is an the acceleration ecosystem for formal methods. open 10.2020 Quasy Quasy is a tool for synthesis of reactive systems which takes qualitative and quantitative specifications in GOAL format. open 07.2011 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 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 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 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 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 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 SMC-LTL Controller Synthesis using SMC open 07.2023 StocHy StocHy simplifies both the modelling and design of stochastic hybrid systems (SHS) and their analysis. open 12.2019 Synthia Synthia is a tool for the verification and synthesis of open real-time systems modeled as timed automata. open 12.2011 SySCoRe SySCoRe is a MATLAB toolbox for temporal logic control synthesis of discrete-time continuous-state stochastic dynamical systems. open 12.2022 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 TuLiP TuLiP is a tool for automatic synthesis of correct-by-construction embedded control software. open 11.2016 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 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 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 PolyAR Polynomial Inequality Constraints Solver (for controller synthesis and reachability analysis) open 07.2023 SCOTS2FPGA SCOTS2FPGA provides space efficient implementations of symbolic controllers on FPGAs. open 06.2019 SL2SX SL2SX is a tool that translates Simulink models (saved in XML format) into SpaceEx models (respecting the SX format). open 12.2017 Wordgen Time word generator open 02.2023
