• SPASS

  • Referenced in 177 articles [sw04108]
  • because validity in first-order logic is undecidable, SPASS may run forever without producing...
  • CoLoR

  • Referenced in 38 articles [sw09806]
  • termination for specific problems (since it is undecidable in general). Ensuring the reliability of those...
  • WSAT

  • Referenced in 37 articles [sw01022]
  • Asynchronous messaging makes most interesting verification problems undecidable, even when XML message contents are abstracted...
  • Cayenne

  • Referenced in 29 articles [sw09686]
  • cost: type checking of Cayenne is undecidable. While this may appear to be a steep...
  • IDLVALID

  • Referenced in 10 articles [sw20417]
  • validity of formulae in these logics is undecidable, for practical applicability there has been considerable...
  • Autowrite

  • Referenced in 8 articles [sw01282]
  • exists. However, neededness is in general undecidable. In order to obtain a decidable approximation...
  • SPeeDI

  • Referenced in 7 articles [sw00896]
  • this and all interesting verification problems are undecidable. Most of the proved decidability results rely...
  • Moby/DC

  • Referenced in 5 articles [sw01395]
  • parameters the model-checking problem is undecidable in general. Hence, we have to accept that...
  • MMCTest

  • Referenced in 5 articles [sw11179]
  • rejected, the non-rejected and the undecided hypotheses. A simulation study motivated by actual biological...
  • BACH

  • Referenced in 4 articles [sw11906]
  • linear hybrid automata, the reachability problem is undecidable. In the author’s previous work...
  • llprover

  • Referenced in 4 articles [sw11993]
  • proof search of linear logic is undecidable. Therefore, this program limits the number of contraction...
  • QPLIB

  • Referenced in 4 articles [sw31286]
  • comprising sub-classes ranging from trivial to undecidable. This diversity is reflected in the variety...
  • pyHybrid Analysis

  • Referenced in 2 articles [sw10940]
  • exhibit a mixed discrete-continuous behaviours. The undecidability of the reach ability problem over them...
  • HoTTSQL

  • Referenced in 2 articles [sw27484]
  • addition, while query equivalence is generally undecidable, we have implemented an automated decision procedure using...
  • Vadalog

  • Referenced in 2 articles [sw33095]
  • presence of existential quantification is in general undecidable. Many efforts have been made to define...
  • SAHA-Tool

  • Referenced in 1 article [sw10315]
  • both discrete and continuous laws. Unfortunately, undecidability soon emerges when one tries to automatically verify...
  • ProbReach

  • Referenced in 1 article [sw20157]
  • required probability. Standard (non-probabilistic) reachability is undecidable even for linear hybrid systems. In ProbReach...
  • RAML

  • Referenced in 1 article [sw21728]
  • solver. Since symbolic bound inference is an undecidable problem, RAML cannot automatically derive a bound...
  • Bellerophon

  • Referenced in 1 article [sw23943]
  • computer control with physical motion. Verification is undecidable for hybrid systems and challenging for many...
  • WNetKAT

  • Referenced in 1 article [sw25228]
  • weighted finite automata, which implies undecidability of the former. However, this paper also shows...