The following tools are developed in the our group:
HyPro is a C++ library collecting the most prominent state set representations used for the reachability analysis of hybrid systems via flowpipe computation. Currently it provides implementations with a unified interface for boxes, convex polytopes, support functions, zonotopes. Furthermore the library holds an implementation of orthogonal polyhedra and also Taylor models.
- Github page: https://github.com/hypro/hypro
- Doxygen API documentation: https://hypro.github.io/hypro/html/
- Pdf manual: manual
Contact: Stefan Schupp
Flow*: Reachability Analyzer for Hybrid Systems
Flow* is a tool to compute Taylor model flowpipes for continuous and hybrid systems. Currently, the tool supports hybrid systems with
- polynomial ODEs,
- mode invariants and jump guards defined by polynomial constraints,
- jump resets defined by polynomial mappings.
Homepage of Flow*
Homepage of some case studies on Flow*
Contact Xin Chen
GiNaCRA – GiNaC Real Algebra package
An open source C++ library extending the C++ library GiNaC which provides algebraic capabilities including support for symbolic manipulations on polynomials. GiNaCRA aims at providing real algebraic computations based on the efficient GiNaC framework.
Available at: http://ginacra.sourceforge.net/
Contact: Ulrich Loup
Computing Minimal Counterexamples for Discrete-Time Markov Chains
COMICS is a stand-alone tool which performs model checking and the generation of counterexamples for discrete-time Markov Chains (DTMCs). For an input DTMC COMICS computes an abstract system that carries the model checking information and uses this result to compute a critical subsystem, which induces a counterexample. This abstract subsystem can be refined and concretized hierarchically
Contact: Nils Jansen
GeneiAL is an open source C++ genetic algorithm library that solves optimization problems. The library has been designed to be extensible to user-specific problems while simultaneously featuring good scalability for the core functionality.
Available at: http://geneial.org
Contact: Johanna Nellen
SpaceEx with CEGAR
We developed an extension of the analysis tool SpaceEx with integrated CEGAR (CounterExample Guided Abstraction Refinement) for the reachability analysis of hybrid systems.
Contact: Johanna Nellen
SMT-RAT is an open-source C++ toolbox for strategic and parallel SMT solving. It contains a collection of SMT compliant implementations for solving different logics, for example linear and nonlinear arithmetic over the reals or integers (QF_LRA, QF_LIA, QF_NRA, QF_NIA) as well as bitvectors (QF_BV).
Contact: Florian Corzilius, Gereon Kremer