• MRMC

  • Referenced in 66 articles [sw04129]
  • Recent tool features include time-bounded reachability analysis for continuous-time Markov decision processes (CTMDPs...
  • Timbuk

  • Referenced in 46 articles [sw06351]
  • 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...
  • VerICS

  • Referenced in 31 articles [sw02011]
  • 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...
  • Uppaal2k

  • Referenced in 43 articles [sw01595]
  • safety and bonded-liveness properties by reachability analysis of the symbolic state-space. Since version...
  • 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...
  • DiVinE

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

  • Referenced in 24 articles [sw01317]
  • modular modeling. The tool provides reachability analysis and refinement checking, both implemented using the data...
  • FLATA

  • Referenced in 15 articles [sw04142]
  • toolset for the manipulation and the analysis of non-deterministic integer programs (also known ... main functionalities of FLATA are: reachability analysis of non-recursive programs - checking if an error ... control state is reachable termination analysis of non-recursive programs - computation of termination preconditions computation...
  • Maria

  • Referenced in 18 articles [sw04127]
  • system nets Maria performs simulation, exhaustive reachability analysis and on-the-fly LTL model checking...
  • RAMAS

  • Referenced in 12 articles [sw10958]
  • Reachability analysis of multi-affine systems. We present a technique for reachability analysis of continuous...
  • Breach

  • Referenced in 17 articles [sw20822]
  • simulation-based techniques aimed at the analysis of deterministic models of hybrid dynamical systems ... latter is used to perform approximate reachability analysis and parameter synthesis. A major novel feature...
  • dReach

  • Referenced in 10 articles [sw20164]
  • dReach:(δ)-reachability analysis for hybrid systems. dReach is a bounded reachability analysis tool...
  • VHPOP

  • Referenced in 10 articles [sw20688]
  • such as distance based heuristics and reachability analysis. We present an adaptation of the additive...
  • FORCE

  • Referenced in 9 articles [sw09016]
  • accelerate SAT-solving. Applications to reachability analysis have also been successful [12]. The main drawback...
  • CORA

  • Referenced in 6 articles [sw25659]
  • verification of cyber-physical systems using reachability analysis. CORA integrates various vector and matrix ... operations on them as well as reachability algorithms of various dynamic system classes. The software ... having to modify the code for reachability analysis. CORA is designed using the object oriented...
  • DISCOVERER

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

  • Referenced in 5 articles [sw02719]
  • present a new algorithm for the reachability analysis of multi-affine hybrid systems ... previous work on reachability analysis and that of our collaborators, we exploited the convexity ... explicitly calculate conical overapproximations of the reachable set in the invariant of each ... mode. We describe our Multi-Affine Reachability analysis using Conical Overapproximations, MARCO, and show that...
  • MARCIE

  • Referenced in 8 articles [sw12882]
  • MARCIE -- model checking and reachability analysis done efficiently. MARCIE is a tool for the analysis...
  • DSSZ-MC

  • Referenced in 6 articles [sw01360]
  • model checking by limited backward reachability analysis. The tool is available for Windows, Linux...
  • Verics

  • Referenced in 6 articles [sw09464]
  • automata, and two complementary methods of reachability analysis. The first one is based on Bounded...