• PKind

  • Referenced in 6 articles [sw21027]
  • PKind: A parallel k-induction based model checker. PKind is a novel parallel k-induction ... incremental invariant generators to enhance basic k-induction. We describe PKind’s functionality and main...
  • SAL

  • Referenced in 8 articles [sw13318]
  • model checkers can prove invariants by k-induction. SAL has been available since...
  • SCRATCH

  • Referenced in 2 articles [sw06537]
  • which uses bounded model checking and k-induction to automatically analyse software for multicore processors...
  • JKind

  • Referenced in 1 article [sw21029]
  • JKind uses parallel cooperating engines including k-induction, property directed reachability, and template-based invariant...
  • HyComp

  • Referenced in 1 article [sw20163]
  • based verification techniques (e.g. BMC, K-induction, IC3). The tool features specialized encodings...
  • HySAT

  • Referenced in 23 articles [sw01980]
  • HySAT: An efficient proof engine for bounded model...
  • TASS

  • Referenced in 2 articles [sw02740]
  • TASS (Timing Analyzer of Scenario-based Specifications) is...
  • HyTech

  • Referenced in 320 articles [sw04125]
  • HyTech is an automatic tool for the analysis...
  • NuSMV

  • Referenced in 288 articles [sw04131]
  • NuSMV is a symbolic model checker developed as...
  • MathSAT

  • Referenced in 56 articles [sw09449]
  • The MathSAT 4 SMT Solver. We present MathSAT...
  • HyDI

  • Referenced in 3 articles [sw11912]
  • HyDI: a language for symbolic hybrid systems with...