• PKind

  • Referenced in 7 articles [sw21027]
  • novel parallel k-induction-based model checker of invariant properties for finite- or infinite-state ... incorporation of incremental invariant generators to enhance basic k-induction. We describe PKind’s functionality ... safety properties and, due to incremental invariant generation, also considerably increases the number of provable...
  • Booster

  • Referenced in 6 articles [sw33291]
  • allowing Booster to efficiently generate required quantified safe inductive invariants attesting the safety...
  • JKind

  • Referenced in 1 article [sw21029]
  • engines including k-induction, property directed reachability, and template-based invariant generation. Downloads: JKind...
  • Aligators

  • Referenced in 1 article [sw09779]
  • tool for the generation of universally quantified array invariants. Aligators leverages recurrence solving and algebraic ... techniques to carry out inductive reasoning over array content. The Aligators’ loop extraction module allows...
  • ACL2

  • Referenced in 283 articles [sw00060]
  • ACL2 is both a programming language in which...
  • CoCoA

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

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

  • Referenced in 65 articles [sw00177]
  • CUTE: a concolic unit testing engine for C...
  • GAP

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

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

  • Referenced in 3315 articles [sw00540]
  • Computer algebra system (CAS). Magma is a large...
  • Maple

  • Referenced in 5373 articles [sw00545]
  • The result of over 30 years of cutting...
  • MATCONT

  • Referenced in 443 articles [sw00551]
  • MATCONT: Matlab software for bifurcation study of dynamical...
  • Mathematica

  • Referenced in 6355 articles [sw00554]
  • Almost any workflow involves computing results, and that...
  • Matlab

  • Referenced in 13544 articles [sw00558]
  • MATLAB® is a high-level language and interactive...
  • MetiTarski

  • Referenced in 52 articles [sw00573]
  • Many inequalities involving the functions ln, exp, sin...
  • MiniSat

  • Referenced in 566 articles [sw00577]
  • An extensible SAT-solver. MiniSat is a minimalistic...
  • NAG

  • Referenced in 423 articles [sw00610]
  • Produced by experts for use in a variety...
  • QEPCAD

  • Referenced in 283 articles [sw00752]
  • QEPCAD B: A program for computing with semi...