• Cadence SMV

  • Referenced in 27 articles [sw07795]
  • Cadence SMV is a symbolic model checking tool that allows you to formally verify temporal ... formal verification is often equated with equivalence checking, model checking is substantially more general...
  • CAESAR_SOLVE

  • Referenced in 14 articles [sw10194]
  • finite-state concurrent systems, such as equivalence checking and model checking. These problems ... three purposes: on-the-fly equivalence checking modulo five widely used equivalence relations...
  • SymDiff

  • Referenced in 16 articles [sw13093]
  • SymDiff, a language-agnostic tool for equivalence checking and displaying semantic (behavioral) differences over imperative...
  • MWB

  • Referenced in 33 articles [sw04395]
  • version of the MWB is checking open bisimulation equivalences. We illustrate the MWB with...
  • WoLFram

  • Referenced in 15 articles [sw02075]
  • verification of PLC programs. Equivalence checking and property checking are applied to prove the correctness...
  • BISIMULATOR

  • Referenced in 7 articles [sw02526]
  • modular tool for on-the-fly equivalence checking. The equivalence checking problem consists in verifying ... Labeled Transition Systems (Ltss) modulo a given equivalence relation ... approaches are traditionally used to perform equivalence checking: global verification requires to construct...
  • CAESAR

  • Referenced in 8 articles [sw29138]
  • generated graph, including model checking, equivalence checking, and visual checking. Taking as input filename.lotos, which...
  • CoVaC

  • Referenced in 7 articles [sw21472]
  • program analysis techniques, we reduce the equivalence checking problem to analysis of one system ... approach can be effectively used for checking equivalence of consonant (i.e., structurally similar) programs. Finally...
  • Sigma*

  • Referenced in 10 articles [sw21731]
  • that can be effectively composed and equivalence checked. Thus, Sigma* enables fully automatic analysis...
  • Concurrency Workbench

  • Referenced in 12 articles [sw14749]
  • allows for various equivalence, preorder and model checking using a variety of different process semantics ... given process, or checking various semantic equivalences and preorders; define propositions in a powerful modal...
  • Beaver

  • Referenced in 9 articles [sw00071]
  • security (rich in nonlinear arithmetic) and equivalence checking (rich Boolean structure...
  • Akiss

  • Referenced in 13 articles [sw20605]
  • Akiss is a verification tool for checking trace equivalence of security protocols. It works...
  • SuSy 2

  • Referenced in 16 articles [sw09258]
  • Hamiltonians (up to SuSy divergence equivalence), and the checking of the validity of the Jacobi...
  • SPEC

  • Referenced in 4 articles [sw20606]
  • authentication. SPEC implements a process equivalence checking procedure based on the paper by Alwen...
  • MDGs

  • Referenced in 3 articles [sw12127]
  • property checking, 3) State enumeration 4) Equivalence checking of two state machines 5) Model checking...
  • QuteRTL

  • Referenced in 2 articles [sw12872]
  • various RTL designs and applied formal equivalence checking with third party tool to verify...
  • BinSim

  • Referenced in 1 article [sw31767]
  • diffing via system call sliced segment equivalence checking. Detecting differences between two binary executables (binary ... propose system call sliced segment equivalence checking, a hybrid method to identify fine-grained semantic ... whether two executable binaries’ behaviors are conditionally equivalent; 2) detecting the similarities or differences, whose...
  • TVOC

  • Referenced in 19 articles [sw02521]
  • check the validity of compiler optimizations: for a given source program, TVOC proves the equivalence...
  • XPi

  • Referenced in 7 articles [sw09430]
  • full agreement with type checking. A notion of barbed equivalence is defined that takes into...
  • Helena

  • Referenced in 6 articles [sw33425]
  • translate Helena specifications into Promela and check satisfaction of LTL properties with Spin ... Helena and Promela and establish stutter trace equivalence between them. Thus, we can guarantee that...