• MAGIC

  • Referenced in 37 articles [sw14159]
  • accuracy and scalability by an iterative abstraction refinement methodology. This paper presents the core principles ... specification conformance using simulation and abstraction refinement. Viewing counterexamples as winning strategies in a simulation ... specification, we describe an algorithm where abstractions are refined on the basis of multiple winning...
  • MathSAT

  • Referenced in 56 articles [sw09449]
  • unsatisfiable cores and Craig interpolants (for abstraction refinement...
  • ARMC

  • Referenced in 26 articles [sw04949]
  • Choice for Software Model Checking with Abstraction Refinement. Software model checking with abstraction refinement ... applies logical reasoning to deal with abstraction. It is therefore natural to investigate whether ... such a tool, called ARMC (for Abstraction Refinement Model Checking), which has already been used...
  • SatAbs

  • Referenced in 38 articles [sw12804]
  • tool, SatAbs, that implements a predicate abstraction refinement loop. Existing software verification tools such ... Blast, or Magic use decision procedures for abstraction and simulation that are limited to integers...
  • Benchmarks

  • Referenced in 24 articles [sw04612]
  • hybrid systems by constraint propagation based abstraction refinement This paper deals with the problem ... this method into an abstraction refinement framework and improve it by developing an additional refinement...
  • CEGAR

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

  • Referenced in 81 articles [sw00025]
  • natural hierarchy of locally refined meshes and an abstract concept of general finite element spaces...
  • 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 ... allows some user control over the abstraction and refinement steps. This paper examines the effect ... various available options for abstraction and refinement. Based on our initial experience with this system...
  • Dagger

  • Referenced in 15 articles [sw04953]
  • Automatically refining abstract interpretations. Abstract interpretation techniques prove properties of programs by computing abstract fixpoints ... present three techniques to automatically refine such abstract interpretations to reduce false errors ... refinement algorithm, which refines abstract interpretations that use the join operator to merge abstract states ... programs that are beyond current abstraction-refinement tools, such as Slam, Blast, Armc...
  • Zapato

  • Referenced in 11 articles [sw25425]
  • zapato: Automatic theorem proving for predicate abstraction refinement. Counterexample-driven abstraction refinement is an automatic ... process that produces abstract models of finite and infinite-state systems. When this process ... feasibility of program paths and to refine the abstraction. In this paper we report ... solve the queries produced during the abstraction refinement process...
  • HSF

  • Referenced in 9 articles [sw09937]
  • based on predicate abstraction and refinement following the CEGAR paradigm. There are a number ... CPAChecker that are also based on abstraction refinement. By using abstraction refinement, HSF(C) finds...
  • YASM

  • Referenced in 12 articles [sw09470]
  • based on the Counter-Example Guided Abstraction Refinement (CEGAR) [6] framework. A number of well ... Traditional software model-checkers build over-approximating abstractions of the programs they analyze and typically...
  • Sigma*

  • Referenced in 8 articles [sw21731]
  • programs and counterexample guided abstraction refinement to over-approximate program behavior, Sigma* transforms arbitrary source ... converges to a complete model if abstraction refinement eventually builds up a sufficiently strong abstraction...
  • Jakarta

  • Referenced in 18 articles [sw01269]
  • manipulate and transform JSL specifications by abstraction and refinement; the JaKarTa Prover Interface ... derive certified Byte Code Verifiers by abstraction from the specification of the JavaCard Virtual Machine...
  • CTIGAR

  • Referenced in 6 articles [sw23310]
  • Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR). Typical CEGAR-based verification methods refine the abstract ... individual states suggests a simpler abstraction-refinement scheme in which refinements are performed relative ... Experiments validate that CTI-focused abstraction refinement, or CTIGAR, is competitive with existing CEGAR-based...
  • UFO

  • Referenced in 19 articles [sw09570]
  • allows definition of different abstract post operators, refinement strategies and exploration strategies. We have built ... three instantiations of the framework: a predicate abstraction-based version, an interpolation-based version...
  • csp2B

  • Referenced in 21 articles [sw07703]
  • csp2B means that abstract specifications and refinements may be specified purely using CSP or using...
  • Specware

  • Referenced in 25 articles [sw11715]
  • with a simple, abstract model of their problem and iteratively refine this model until...
  • SLAB

  • Referenced in 8 articles [sw09875]
  • uses a procedure that interleaves automatic abstraction refinement using Craig interpolation with slicing, which removes...
  • Synthia

  • Referenced in 8 articles [sw12933]
  • algorithm is based on a novel abstraction refinement technique that enables a clean combination...