Tools

The following tools are developed in the our group:

HyPro: A C++ state set representation library for the analysis of hybrid systems

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.

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

COMICS

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

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

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