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

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

Timbuk
 Referenced in 47 articles
[sw06351]
 tree automata) Timbuk and reachability analysis can be used for program verification. For instance, Timbuk ... tree automata completion engine used for reachability analysis. Older Timbuk distributions (2.2) provide three standalone...

FLATA
 Referenced in 19 articles
[sw04142]
 functionalities of FLATA are: reachability analysis of nonrecursive programs  checking if an error control ... state is reachable termination analysis of nonrecursive programs  computation of termination preconditions computation...

MOPS
 Referenced in 23 articles
[sw10117]
 this process. Our program analysis models the program to be verified as a pushdown automaton ... desired security goal is reachable in the program. The major advantages of this approach...

Memorax
 Referenced in 4 articles
[sw09759]
 verification of control state reachability (i.e., safety properties) of concurrent programs manipulating finite range ... arbitrary or even infinite sizes. Even for programs that only manipulate finite range variables ... verification of control state reachability for concurrent programs involving integer variables. The reachability procedure ... control states under TSO. In fact, for programs only involving finite range variables and running...

TRACER
 Referenced in 12 articles
[sw09484]
 symbolic execution for finitestate C sequential programs developed at National University of Singapore . TRACER ... which overapproximates the set of all concrete reachable states. If the error location cannot ... reached from any symbolic path then the program is reported as safe. Otherwise, either...

Stranger
 Referenced in 16 articles
[sw09152]
 reachability analyses to compute the possible values that the string expressions can take during program...

Boom
 Referenced in 2 articles
[sw01318]
 where thread counters are used in a programcontext aware way. While designed for bounded ... addition systems, resulting in a reachability engine for programs with unbounded thread creation. The concurrent...

JayHorn
 Referenced in 2 articles
[sw25903]
 states in a Java program are never reachable. These bad states are specified by adding...

Maria
 Referenced in 19 articles
[sw04127]
 algebraic system nets Maria performs simulation, exhaustive reachability analysis and onthefly LTL model ... Petri nets and labelled transition systems. Translator programs allow Maria to analyse transition systems...

PARTS
 Referenced in 2 articles
[sw03123]
 uses a Petrinetbased reachability analysis to analyze program specifications written...

Mcmt
 Referenced in 24 articles
[sw11911]
 core of the system is a backward reachability procedure which symbolically computes preimages ... successfully applied to the verification of imperative programs, parametrised, timed, and distributed systems...

Skink
 Referenced in 1 article
[sw28628]
 program analysis is “correct” if the error block is not reachable, “incorrect ... error block is reachable, or “inconclusive” if the status of the program could...

BACH
 Referenced in 4 articles
[sw11906]
 simple class of linear hybrid automata, the reachability problem is undecidable. In the author ... linear hybrid automata we proposed a linear programming based approach to check one path ... prototype tool BACH to perform bounded reachability checking of linear hybrid automata. The experiment data...

nlpden
 Referenced in 3 articles
[sw09371]
 reachable under the additive noise model. Our estimator reduces to a quadratic program...

NLTOOLBOX
 Referenced in 3 articles
[sw09248]
 library of data structures and algorithms for reachability computation of nonlinear dynamical systems. It provides ... users with an easy way to “program” their own analysis procedures or to solve other...

MLAT
 Referenced in 3 articles
[sw00582]
 programs. The logic has enough expressive power to describe properties of heaps, such as reachability...

gridlib
 Referenced in 6 articles
[sw00390]
 assists with the transparent use of parallel programming concepts, modular structure and clean interfaces ... adaptive, hierarchical unstructured approach to grids. The reachable performance of these algorithms in the domain...

DDebugger
 Referenced in 15 articles
[sw09904]
 from an incorrect computation and locates a program fragment responsible for the error by building ... rewriting logic, and rewrites and sets of reachable terms through rules. We use an abbreviation...