
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 overapproximation of the reachable states. The algorithm improves over previous work...

MRMC
 Referenced in 71 articles
[sw04129]
 support for computing time and rewardbounded reachability probabilities, (propertydriven) bisimulation minimization, and precise ... detection. Recent tool features include timebounded reachability analysis for continuoustime 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 timeoptimal 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 (onthefly) 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 bondedliveness properties by reachability analysis of the symbolic statespace. 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 (BDDbased ... reachability, distributed reachability (MPIbased), and multicore reachability (including multicore compression and incremental...

PAT
 Referenced in 36 articles
[sw13258]
 properties such as deadlockfreeness, divergencefreeness, 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 firstorder 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 nonrecursive programs  checking ... error control state is reachable termination analysis of nonrecursive 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 ... cyberphysical 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]
 modelchecking 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...