• fminsearch

  • Referenced in 262 articles [sw07467]
  • limited convergence results for dimension 2. A counterexample of McKinnon gives a family of strictly...
  • Prover9

  • Referenced in 180 articles [sw04969]
  • Mace4 searches for finite models and counterexamples. Prover9 is the successor of the Otter prover...
  • GRAFFITI

  • Referenced in 169 articles [sw07495]
  • graphs known by the program is an counterexample. The structure and the performances...
  • Nitpick

  • Referenced in 61 articles [sw00622]
  • Nitpick is a counterexample generator for Isabelle/HOL that builds on Kodkod, a SAT-based first ... TPTP library indicate that Nitpick generates more counterexamples than other model finders for higher-order...
  • MathSAT

  • Referenced in 58 articles [sw09449]
  • this setting. In particular: model generation (for counterexample reconstruction), model enumeration (for predicate abstraction...
  • House of Graphs

  • Referenced in 44 articles [sw06693]
  • study of graph theoretic problems or as counterexamples to conjectures. This list can be extended...
  • MAGIC

  • Referenced in 37 articles [sw14159]
  • conformance using simulation and abstraction refinement. Viewing counterexamples as winning strategies in a simulation game...
  • CEGAR

  • Referenced in 33 articles [sw04605]
  • Counterexample-guided abstraction refinement (CEGAR) has been en vogue for the automatic verification of very...
  • PROMELA

  • Referenced in 30 articles [sw07635]
  • given system, or it generates a counterexample that shows that it is not. This paper...
  • Reveal

  • Referenced in 20 articles [sw00801]
  • four representative hardware test cases. Reveal employs counterexample-guided abstraction refinement, or CEGAR ... automatically refined based on the spurious counterexample it generates. Such refinement can be viewed...
  • TestEra

  • Referenced in 22 articles [sw07258]
  • structures. TestEra produces concrete Java inputs as counterexamples to violated correctness criteria. The paper discusses...
  • Checkfence

  • Referenced in 19 articles [sw09939]
  • test fails, CheckFence provides an HTML-formatted counterexample trace that displays various views...
  • CLICAL

  • Referenced in 17 articles [sw20733]
  • help of CLICAL, I have found counterexamples to conjectures and theorems about Clifford algebras...
  • MathCheck

  • Referenced in 11 articles [sw13642]
  • assistant by mathematicians to either counterexample or finitely verify open universal conjectures on any mathematical ... specific lemmas, as it searches for a counterexample to the input conjecture (just like...
  • Spacer

  • Referenced in 11 articles [sw19496]
  • Over-approximations are used to block infeasible counterexamples and detect convergence to a proof ... algorithm is guaranteed to find a counterexample, if one exists. However, efficiency depends...
  • HipSpec

  • Referenced in 14 articles [sw07736]
  • uses a novel approach, combining theory exploration, counterexample testing and inductive theorem proving. HipSpec automatically...
  • CTIGAR

  • Referenced in 7 articles [sw23310]
  • Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR). Typical CEGAR-based verification methods refine the abstract ... domain based on full counterexample traces. The finite state model checking algorithm IC3 introduced ... generalizing from, and thereby eliminating individual state counterexamples to induction (CTIs). This focus on individual...
  • Leon

  • Referenced in 11 articles [sw09159]
  • smaller satisfiable formulas and ensures completeness for counterexamples. We illustrate the current capabilities of Leon...
  • TRACER

  • Referenced in 11 articles [sw09484]
  • from infeasible paths and integrates a novel counterexample-guided refinement phase within the symbolic execution...
  • Zapato

  • Referenced in 11 articles [sw25425]
  • Automatic theorem proving for predicate abstraction refinement. Counterexample-driven abstraction refinement is an automatic process...