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

SpaceEx
 Referenced in 72 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 70 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 42 articles
[sw12913]
 timed game automata with respect to reachability and safety properties. Though timed games for long ... obtaining timeoptimal winning strategies (for reachability games...

DISCOVERER
 Referenced in 56 articles
[sw07719]
 analysis and invariant generation of programs, and reachability computation of hybrid systems...

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

VerICS
 Referenced in 33 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...

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...

Uppaal2k
 Referenced in 43 articles
[sw01595]
 safety and bondedliveness properties by reachability analysis of the symbolic statespace. Since version...

MATISSE
 Referenced in 26 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...

LTSmin
 Referenced in 18 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 33 articles
[sw13258]
 properties such as deadlockfreeness, divergencefreeness, reachability, LTL properties with fairness assumptions, refinement checking...

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

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...

FLATA
 Referenced in 18 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...

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

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