• Coq/SSReflect

  • Referenced in 62 articles [sw09360]
  • library arithmetic comparison is not an abstract predicate, but a function computing a boolean...
  • FOCI

  • Referenced in 58 articles [sw12868]
  • verification, for example, discovering predicates in predicate abstraction, and computing inductive invariants...
  • MathSAT

  • Referenced in 56 articles [sw09449]
  • counterexample reconstruction), model enumeration (for predicate abstraction), an incremental interface (for BMC), and computation...
  • VeriFast

  • Referenced in 56 articles [sw07705]
  • separation logic assertion. Folding or unfolding abstract predicate assertions is performed through explicit ghost statements...
  • SatAbs

  • Referenced in 38 articles [sw12804]
  • SATABS: SAT-based predicate abstraction for ANSI-C. This paper presents a model checking tool ... SatAbs, that implements a predicate abstraction refinement loop. Existing software verification tools such as Slam...
  • jStar

  • Referenced in 32 articles [sw11261]
  • verification: it combines the idea of abstract predicate families and the idea of symbolic execution...
  • 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...
  • UFO

  • Referenced in 19 articles [sw09570]
  • verification algorithms. It allows definition of different abstract post operators, refinement strategies and exploration strategies ... three instantiations of the framework: a predicate abstraction-based version, an interpolation-based version ... powerful combination of interpolation-based and predicate abstraction-based algorithms...
  • MAGIC

  • Referenced in 37 articles [sw14159]
  • this aim, MAGIC extracts abstract software models using predicate ahstraction, and resolves the inherent trade ... model accuracy and scalability by an iterative abstraction refinement methodology. This paper presents the core...
  • UCLID

  • Referenced in 25 articles [sw04657]
  • checking, correspondence checking, deductive verification, and predicate abstraction-based verification. As a stand-alone decision...
  • Zapato

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

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

  • Referenced in 9 articles [sw09937]
  • programs. HSF(C) is based on predicate abstraction and refinement following the CEGAR paradigm. There...
  • PASS

  • Referenced in 7 articles [sw04431]
  • probabilistic models. It is based on predicate abstraction and automatic abstraction refinement. Models are specified...
  • KRATOS

  • Referenced in 7 articles [sw07808]
  • programs using the symbolic lazy predicate abstraction technique. Second, Kratos implements a novel algorithm, called...
  • Hiord

  • Referenced in 4 articles [sw07313]
  • higher-order logic programming language with predicate abstraction A new formalism, called Hiord, for defining ... higher-order logic programming languages with predicate abstraction is introduced. A model theory, based...
  • MLAT

  • Referenced in 3 articles [sw00582]
  • framework based on modal logic and predicate abstraction technique. In the framework we employ modal ... logic 2CTLN in order to express predicates for abstraction and specifications of programs. The logic ... such as reachability. Moreover it fits predicate abstraction scheme because its satisfiability problem is decidable...
  • SymmPa

  • Referenced in 3 articles [sw08414]
  • abstraction refinement for symmetric concurrent programs. Predicate abstraction and counterexample-guided abstraction refinement (CEGAR) have...
  • monabs

  • Referenced in 2 articles [sw18507]
  • odds with monotonicity: predicate-abstracting monotone software can result in non-monotone Boolean programs ... inapplicable. We demonstrate how monotonicity in the abstraction can be restored, without affecting safety properties ... numerous concurrent programs and algorithms, whose predicate abstractions are often fundamentally beyond existing tools...
  • EUREKA

  • Referenced in 3 articles [sw20979]
  • experiments, techniques based on predicate abstraction do not apply successfully...