• BLAST

  • Referenced in 123 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 104 articles [sw12277]
  • tradeoffs, query processing on spatial networks, and reachability queries; and theoretical computer scientists analyze distance...
  • MRMC

  • Referenced in 66 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...
  • SpaceEx

  • Referenced in 62 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...
  • Timbuk

  • Referenced in 46 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 38 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 31 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...
  • d/dt

  • Referenced in 35 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...
  • Uppaal2k

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

  • Referenced in 25 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...
  • DISCOVERER

  • Referenced in 40 articles [sw07719]
  • analysis and invariant generation of programs, and reachability computation of hybrid systems...
  • DiVinE

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

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

  • Referenced in 14 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...
  • Maria

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

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

  • Referenced in 24 articles [sw01317]
  • concepts for modular modeling. The tool provides reachability analysis and refinement checking, both implemented using...
  • LoLA

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

  • Referenced in 23 articles [sw10117]
  • state violating the desired security goal is reachable in the program. The major advantages...
  • FLATA

  • Referenced in 15 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...