• CEGAR

  • Referenced in 34 articles [sw04605]
  • Counterexample-guided abstraction refinement (CEGAR) has been en vogue for the automatic verification of very ... past years. When trying to apply CEGAR to the verification of probabilistic systems, various foundational...
  • CPAchecker

  • Referenced in 54 articles [sw07408]
  • predicate analysis with adjustable-block encoding and CEGAR...
  • Reveal

  • Referenced in 21 articles [sw00801]
  • Reveal employs counterexample-guided abstraction refinement, or CEGAR, and is suitable for verifying the complex...
  • CAQE

  • Referenced in 16 articles [sw25922]
  • certifying QBF solver. We present a new CEGAR-based algorithm for QBF. The algorithm builds...
  • YASM

  • Referenced in 13 articles [sw09470]
  • Counter-Example Guided Abstraction Refinement (CEGAR) [6] framework. A number of well-engineered software model...
  • HSF

  • Referenced in 12 articles [sw09937]
  • predicate abstraction and refinement following the CEGAR paradigm. There are a number of successful tools...
  • CTIGAR

  • Referenced in 8 articles [sw23310]
  • Induction-Guided Abstraction-Refinement (CTIGAR). Typical CEGAR-based verification methods refine the abstract domain based ... refinement, or CTIGAR, is competitive with existing CEGAR-based tools...
  • MoCHi

  • Referenced in 11 articles [sw21478]
  • higher-order model checking, predicate abstraction, and CEGAR (see this paper for details...
  • HARE

  • Referenced in 4 articles [sw10938]
  • Hybrid automata-based CEGAR for rectangular hybrid systems. In this paper we present a framework ... carrying out counterexample guided abstraction-refinement (CEGAR) for systems modelled as rectangular hybrid automata ... between our approach and previous proposals for CEGAR for hybrid automata, is that we consider ... automata as well. We show that the CEGAR scheme is semi-complete for the class...
  • SymmPa

  • Referenced in 3 articles [sw08414]
  • Predicate abstraction and counterexample-guided abstraction refinement (CEGAR) have enabled finite-state model checking ... little evidence of fruitful applications of CEGAR to shared-variable concurrent software. We attribute this ... have developed a symmetry-aware CEGAR technique: it takes into account the replicated structure...
  • ACSAR

  • Referenced in 4 articles [sw02684]
  • based on the counterexample-guided abstraction refinement (CEGAR) paradigm. Its specificity lies...
  • Memorax

  • Referenced in 4 articles [sw09759]
  • addition, Memorax incorporates an interpolation based CEGAR loop to make possible the verification of control...
  • Ultimate Kojak

  • Referenced in 4 articles [sw23308]
  • programs. It is based on CEGAR and Craig interpolation. The basic algorithm, described...
  • McScM

  • Referenced in 1 article [sw14482]
  • verification tool implements several model-checking techniques: CEGAR with different abstraction-refinement methods, abstract interpretation...
  • Ultimate Taipan

  • Referenced in 1 article [sw28629]
  • programs. It is based on a CEGAR variant, trace abstractionï¾ź[7], where program abstractions...
  • MiniSat

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

  • Referenced in 9810 articles [sw00771]
  • R is a language and environment for statistical...
  • PRISM

  • Referenced in 442 articles [sw01186]
  • PRISM: Probabilistic symbolic model checker. In this paper...
  • HySAT

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

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