• LANGAGE

  • Referenced in 39 articles [sw00501]
  • LANGAGE is a set of procedures for deciding whether or not a language given ... last properties. This package is written using the symbolic computation system Maple. It works with...
  • FMona

  • Referenced in 3 articles [sw00303]
  • used to build a reduced system with decidable properties. The FMona tool is used ... leading to synthesis of a finite abstract system then SMV and/or Mona validate its properties...
  • GAVS

  • Referenced in 9 articles [sw00323]
  • properties of computer systems can often be reduced to deciding the winner of a game...
  • UPPAAL TIGA

  • Referenced in 46 articles [sw12913]
  • safety properties. Though timed games for long have been known to be decidable there ... linear-time model-checking of finite-state systems. Being on-the-fly, the symbolic algorithm...
  • FORT

  • Referenced in 2 articles [sw28637]
  • used to decide properties of a given rewrite system and to synthesize rewrite systems that...
  • SPeeDI

  • Referenced in 8 articles [sw00896]
  • systems this and all interesting verification problems are undecidable. Most of the proved decidability results ... properties of the specific (class of) systems under analysis. An interesting and still decidable class...
  • ACE

  • Referenced in 9 articles [sw22675]
  • this evaluation. The ACE (Automatic Complexity Evaluator) system is able to analyze reasonably large programs ... complexity is not a decidable property, this transformation will not be possible in all cases ... predefined library is, the more likely the system is to succeed. The operations performed...
  • Autowrite

  • Referenced in 8 articles [sw01282]
  • Autowrite: A tool for checking properties of term rewriting systems Huet and Lévy have shown ... class of orthogonal term rewriting systems (TRSs) every term not in normal form contains ... general undecidable. In order to obtain a decidable approximation to neededness Huet and Lévy introduced ... showed that strong sequentiality is a decidable property of orthogonal TRSs...
  • COFFEE

  • Referenced in 22 articles [sw20274]
  • pattern in a kernel, and then autonomously decide on the application of padding and data ... currently used in Firedrake, an automated system for the solution of partial differential equations using ... designed to exploit a fundamental mathematical property of finite element integration kernels, namely linearity...
  • Charlie

  • Referenced in 4 articles [sw12881]
  • siphon/trap property) to determine structural and behavioural properties of place/transition Petri nets, complemented by explicit ... rule system comprising standard theorems of Petri net theory to possibly decide further properties based ... model verification of technical systems, especially software-based systems, as well as for model validation...
  • DLV-EX

  • Referenced in 16 articles [sw04642]
  • very large polynomially decidable class having this property, when no assumption can be made about ... eventually discussed, and the implementation of a system supporting the class of such programs...
  • DifferentialAlgebra

  • Referenced in 11 articles [sw13540]
  • deciding membership to a differential ideal, and ReducedForm for reducing a system with respect ... differential equation systems is PowerSeriesSolution. Other commands for analyzing mathematical properties of differential systems...
  • Ivy

  • Referenced in 10 articles [sw41668]
  • proving safety and liveness properties of parameterized and infinite-state systems via three modes: deductive ... code. It is designed to support decidable automated reasoning, to improve proof stability...
  • PLASMA

  • Referenced in 5 articles [sw18420]
  • checking offers the potential to decide and quantify dynamical properties of models with intractably large ... verify the performance of complex real-world systems. Rare properties and long simulations pose...
  • KRIPKE

  • Referenced in 8 articles [sw01162]
  • just the axiom that governs the distributional properties ... obtain the system called O R in [10] and studied in this book. A theorem ... modal S4 are decidable. This theorem was shown in [8] to be equivalent...
  • OreAlgebraicAnalysis

  • Referenced in 4 articles [sw15153]
  • homological algebra techniques. The different types of systems can be uniformly described by using ... algebras, (2) algorithms for deciding module-theoretic properties, such as torsion-freeness, reflexivity, projectiveness, freeness...
  • monabs

  • Referenced in 2 articles [sw18507]
  • systems stipulates that, in any global state, system actions remain executable when new processes ... finite, monotonicity often guarantees the decidability of safety properties even when the number of running ... established safety checking algorithms for infinite-state systems become inapplicable. We demonstrate how monotonicity...
  • RDL

  • Referenced in 4 articles [sw26677]
  • success of state-of-the-art verification systems, such as ACL2, STEP, Tecton, and Simplify ... makes it difficult to reason about basic properties such as soundness and termination ... verification efforts falls exactly into the theory decided by the available decision procedure...
  • LANGAGEA

  • Referenced in 1 article [sw15338]
  • LANGAGE is a set of procedures for deciding whether or not a language given ... last properties. This package is written using the symbolic computation system Maple. It works with...
  • SAHA-Tool

  • Referenced in 1 article [sw10315]
  • powerful formalism for the representation of systems evolving according to both discrete and continuous laws ... automata properties. An important verification problem is the reachability one that demands to decide whether...