
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 SATbased first ... TPTP library indicate that Nitpick generates more counterexamples than other model finders for higherorder...

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]
 Counterexampleguided 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 counterexampleguided 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 HTMLformatted 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]
 Overapproximations 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 InductionGuided AbstractionRefinement (CTIGAR). Typical CEGARbased 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 counterexampleguided refinement phase within the symbolic execution...

Zapato
 Referenced in 11 articles
[sw25425]
 Automatic theorem proving for predicate abstraction refinement. Counterexampledriven abstraction refinement is an automatic process...