• CEGAR

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

  • Referenced in 20 articles [sw00801]
  • test cases. Reveal employs counterexample-guided abstraction refinement, or CEGAR, and is suitable for verifying ... with wide datapaths. Reveal performs automatic datapath abstraction yielding an approximation of the original design ... coarse, it is automatically refined based on the spurious counterexample it generates. Such refinement...
  • ACSAR

  • Referenced in 4 articles [sw02684]
  • based on the counterexample-guided abstraction refinement (CEGAR) paradigm. Its specificity lies ... arises from creating more and more spurious counterexamples by unfolding the same (while...
  • CTIGAR

  • Referenced in 7 articles [sw23310]
  • Induction-Guided Abstraction-Refinement (CTIGAR). Typical CEGAR-based verification methods refine the abstract domain based ... full counterexample traces. The finite state model checking algorithm IC3 introduced the concept of discovering...
  • SymmPa

  • Referenced in 3 articles [sw08414]
  • concurrent programs. Predicate abstraction and counterexample-guided abstraction refinement (CEGAR) have enabled finite-state model...
  • HARE

  • Referenced in 4 articles [sw10938]
  • Hybrid automata-based CEGAR for rectangular hybrid systems. In this paper we present ... framework for carrying out counterexample guided abstraction-refinement (CEGAR) for systems modelled as rectangular hybrid ... proposals for CEGAR for hybrid automata, is that we consider the abstractions to be hybrid ... HyTech to analyze the abstract models and validate the counterexamples. Our experiments demonstrate the usefulness...
  • MiniSat

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

  • Referenced in 127 articles [sw02937]
  • BLAST (Berkeley Lazy Abstraction Software verification Tool) is...
  • HyTech

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

  • Referenced in 169 articles [sw04560]
  • The GLPK (GNU Linear Programming Kit) package is...
  • z3

  • Referenced in 509 articles [sw04887]
  • Z3 is a high-performance theorem prover being...
  • Chaff

  • Referenced in 570 articles [sw06916]
  • Chaff:engineering an efficient SAT solver. Boolean Satisfiability...
  • sQueezeBF

  • Referenced in 15 articles [sw06959]
  • sQueezeBF: an effective preprocessor for QBFs based on...
  • Quaffle

  • Referenced in 64 articles [sw07278]
  • Quaffle: Quantified Boolean Formula Evaluator with Learning Quaffle...
  • CPAchecker

  • Referenced in 50 articles [sw07408]
  • Cpachecker with sequential combination of explicit-state analysis...
  • TRACER

  • Referenced in 11 articles [sw09484]
  • TRACER: A Symbolic Execution Tool for Verification. TRACER...
  • Bloqqer

  • Referenced in 28 articles [sw09578]
  • Blocked clause elimination for QBF. Quantified Boolean formulas...
  • Nenofex

  • Referenced in 18 articles [sw09579]
  • Nenofex: Expanding NNF for QBF Solving. The topic...
  • QUBOS

  • Referenced in 24 articles [sw09580]
  • QUBOS: Deciding quantified Boolean logic using propositional satisfiability...
  • DepQBF

  • Referenced in 31 articles [sw09734]
  • DepQBF is a search-based solver for quantified...