• 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 non-recursive programs - checking if an error control ... state is reachable termination analysis of non-recursive 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 finite-state 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 program-context 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 on-the-fly LTL model ... Petri nets and labelled transition systems. Translator programs allow Maria to analyse transition systems...
  • PARTS

  • Referenced in 2 articles [sw03123]
  • uses a Petri-net-based 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 pre-images ... 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...