• BLAST

  • Referenced in 129 articles [sw02937]
  • tool for C language that solves the reachability problem, i.e. whether a given program location ... safety properties may be reduced to the reachability, and BLAST is used for such verification...
  • Graphs

  • Referenced in 107 articles [sw12277]
  • tradeoffs, query processing on spatial networks, and reachability queries; and theoretical computer scientists analyze distance...
  • SpaceEx

  • Referenced in 74 articles [sw10939]
  • Hybrid Systems. We present a scalable reachability algorithm for hybrid systems with piecewise affine ... compute an over-approximation of the reachable states. The algorithm improves over previous work...
  • MRMC

  • Referenced in 71 articles [sw04129]
  • support for computing time- and reward-bounded reachability probabilities, (property-driven) bisimulation minimization, and precise ... detection. Recent tool features include time-bounded reachability analysis for continuous-time Markov decision processes...
  • Timbuk

  • Referenced in 47 articles [sw06351]
  • collection of tools for achieving proofs of reachability over Term Rewriting Systems and for manipulating ... deterministic finite tree automata) Timbuk and reachability analysis can be used for program verification ... tree automata completion engine used for reachability analysis. Older Timbuk distributions (2.2) provide three standalone...
  • UPPAAL TIGA

  • Referenced in 45 articles [sw12913]
  • timed game automata with respect to reachability and safety properties. Though timed games for long ... obtaining time-optimal winning strategies (for reachability games...
  • VerICS

  • Referenced in 35 articles [sw02011]
  • examples of inputs see here For today, reachability analysis is available. For disproving safety properties ... efficient method consisting in translating the reachability problem for Timed Automata to the satisfiability problem ... proving correctness, an (on-the-fly) reachability analysis on an abstract model of the system...
  • DiVinE

  • Referenced in 56 articles [sw04130]
  • tool for LTL model checking and reachability analysis of discrete distributed systems. The tool...
  • DISCOVERER

  • Referenced in 56 articles [sw07719]
  • analysis and invariant generation of programs, and reachability computation of hybrid systems...
  • d/dt

  • Referenced in 37 articles [sw10314]
  • d/dt is a tool for reachability analysis of continuous and hybrid systems with linear differential ... based on a method for overapproximating reachable sets by orthogonal polyhedra. The tool also allows...
  • MATISSE

  • Referenced in 27 articles [sw06311]
  • free MATLAB toolbox for safety verification and reachable set computation of large dimensional, constrained linear ... checking whether the intersection of the reachable set of the system with an unsafe ... distance of the unsafe set to the reachable set of the abstraction of the system...
  • Uppaal2k

  • Referenced in 43 articles [sw01595]
  • safety and bonded-liveness properties by reachability analysis of the symbolic state-space. Since version...
  • LTSmin

  • Referenced in 21 articles [sw07214]
  • code, and automatically yields tools for standard reachability checking (e.g., for state space generation ... verification of safety properties), reachability with symbolic state storage (vector set), fully symbolic (BDD-based ... reachability, distributed reachability (MPI-based), and multi-core reachability (including multi-core compression and incremental...
  • PAT

  • Referenced in 36 articles [sw13258]
  • properties such as deadlock-freeness, divergence-freeness, reachability, LTL properties with fairness assumptions, refinement checking...
  • dReach

  • Referenced in 18 articles [sw20164]
  • dReach:(δ)-reachability analysis for hybrid systems. dReach is a bounded reachability analysis tool ... nonlinear hybrid systems. It encodes reachability problems of hybrid systems to first-order formulas over...
  • Maria

  • Referenced in 19 articles [sw04127]
  • Maria: Modular reachability analyser for algebraic system nets Maria performs simulation, exhaustive reachability analysis...
  • FLATA

  • Referenced in 19 articles [sw04142]
  • automata). The main functionalities of FLATA are: reachability analysis of non-recursive programs - checking ... error control state is reachable termination analysis of non-recursive programs - computation of termination preconditions...
  • CORA

  • Referenced in 15 articles [sw25659]
  • COntinuous Reachability Analyzer (CORA) is a collection of MATLAB classes for the formal verification ... cyber-physical systems using reachability analysis. CORA integrates various vector and matrix set representations ... operations on them as well as reachability algorithms of various dynamic system classes. The software ... without having to modify the code for reachability analysis. CORA is designed using the object...
  • Romeo

  • Referenced in 26 articles [sw00812]
  • model-checking of reachability properties. It performs translations from TPNs to Timed Automata (TAs) that...
  • LoLA

  • Referenced in 26 articles [sw04381]
  • techniques cover standard properties (liveness, reversibility, boundedness, reachability, dead transitions, deadlocks, home states) as well...