• Vivid

  • Referenced in 3 articles [sw01316]
  • formal semantic framework based on 3-valued logic. We extend the assumption-base semantics...
  • VESTA

  • Referenced in 25 articles [sw08425]
  • statistical evaluation of expected values of temporal expressions. For model-checking VESTA uses a sequence ... property specified in probabilistic computation tree logic (PCTL) [3] or continuous stochastic logic ... VESTA supports the statistical computation of expected values of expressions written in a query language...
  • Racer

  • Referenced in 66 articles [sw09837]
  • Racer is distributed under the following BSD 3-clause license. For downloading Racer ... inference services are provided, such as, e.g., logical abduction. Racer also provides the powerful ... negation as failure, numeric constraints w.r.t. attribute values of different individuals, substring properties between string...
  • MDGs

  • Referenced in 3 articles [sw12127]
  • order logic formulas suitable for high-level hardware verification With MDGs, a data value ... combinational circuits, 2) Safety property checking, 3) State enumeration 4) Equivalence checking of two state...
  • ANSYS

  • Referenced in 713 articles [sw00044]
  • ANSYS offers a comprehensive software suite that spans...
  • Apron

  • Referenced in 71 articles [sw00045]
  • Apron: a library of numerical abstract domains for...
  • ARMS

  • Referenced in 68 articles [sw00048]
  • ARMS: an algebraic recursive multilevel solver for general...
  • ACL2

  • Referenced in 291 articles [sw00060]
  • ACL2 is both a programming language in which...
  • AXIOM

  • Referenced in 173 articles [sw00063]
  • Axiom is a general purpose Computer Algebra system...
  • BIGEBRA

  • Referenced in 21 articles [sw00078]
  • Clifford and Graßmann Hopf algebras via the BIGEBRA...
  • CLIFFORD

  • Referenced in 85 articles [sw00131]
  • CLIFFORD performs various computations in Grass mann and...
  • CoCoA

  • Referenced in 659 articles [sw00143]
  • CoCoA is a system for Computations in Commutative...
  • Coq

  • Referenced in 1906 articles [sw00161]
  • Coq is a formal proof management system. It...
  • COSTA

  • Referenced in 24 articles [sw00162]
  • COSTA is a research prototype which performs automatic...
  • Dafny

  • Referenced in 74 articles [sw00183]
  • Dafny is an imperative object-based language with...
  • GAP

  • Referenced in 3221 articles [sw00320]
  • GAP is a system for computational discrete algebra...
  • IMITATOR

  • Referenced in 31 articles [sw00439]
  • IMITATOR is a software tool for parametric verification...
  • Isabelle

  • Referenced in 719 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • LEDA

  • Referenced in 264 articles [sw00509]
  • In the core computer science areas -- data structures...