• MathSAT

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

  • Referenced in 20 articles [sw09570]
  • Framework for Abstraction- and Interpolation-Based Software Verification. In this paper, we present ... verification algorithms. It allows definition of different abstract post operators, refinement strategies and exploration strategies ... framework: a predicate abstraction-based version, an interpolation-based version, and a combined version which ... novel and powerful combination of interpolation-based and predicate abstraction-based algorithms...
  • FOCI

  • Referenced in 58 articles [sw12868]
  • importantly, it can compute quantifier-free Craig interpolants for inconsistent pairs (or more generally, sequences ... verification, for example, discovering predicates in predicate abstraction, and computing inductive invariants...
  • SAFARI

  • Referenced in 9 articles [sw28669]
  • SAFARI: SMT-Based Abstraction for Arrays with Interpolants. We present SAFARI, a model checker designed ... based on an extension of lazy abstraction capable of handling existentially quantified formulæ for symbolically ... called term abstraction, favors the convergence of the tool by “tuning” interpolants and guessing additional...
  • SLAB

  • Referenced in 8 articles [sw09875]
  • procedure that interleaves automatic abstraction refinement using Craig interpolation with slicing, which removes irrelevant states...
  • Booster

  • Referenced in 5 articles [sw33291]
  • with standard verification techniques, like Lazy Abstraction with Interpolants (extended to arrays). The new acceleration...
  • Dagger

  • Referenced in 15 articles [sw04953]
  • such abstract interpretations to reduce false errors: (1) a new operator called interpolated widen, which ... refinement algorithm, which refines abstract interpretations that use the join operator to merge abstract states...
  • TnT

  • Referenced in 19 articles [sw07977]
  • deleted interpolation. Unknown words are handled by a suffix trie and successive abstraction...
  • RESUME

  • Referenced in 14 articles [sw36118]
  • mechanisms: point temporal abstraction, a mechanism for abstracting the values of several parameters into ... interval or two meeting intervals; and temporal interpolation, a mechanism for bridging nonmeeting temporal intervals ... Making explicit the knowledge required for temporal abstraction supports the acquisition and the sharing...
  • Eldarica

  • Referenced in 3 articles [sw09748]
  • Eldarica system is based on predicate abstraction with interpolation-based counterexample-driven refinement. The Eldarica...
  • eVolCheck

  • Referenced in 6 articles [sw09711]
  • tool maintains abstractions of program functions, function summaries, derived using Craig interpolation. In each check...
  • PZ

  • Referenced in 9 articles [sw09006]
  • dimensional finite elements with arbitrary orders of interpolation and applicable to a variety of systems ... differential equations. The TMatrix environment includes an abstract matrix class interface and a variety...
  • Ultimate Automizer

  • Referenced in 4 articles [sw07407]
  • tool is the first implementation of trace abstraction, which is an automata-theoretic approach ... software verification. The implemented algorithm uses nested interpolants in its interprocedural program analysis. The interpolating...
  • JuAFEM

  • Referenced in 2 articles [sw28361]
  • general and to keep mathematical abstractions. The main functionalities of the package include: Facilitate integration ... different quadrature rules. Define different finite element interpolations. Evaluate shape functions, derivatives of shape functions...
  • Ultimate Taipan

  • Referenced in 1 article [sw28629]
  • computes fixpoints for those path programs using abstract interpretation. If the fixpoints are strong enough ... strong enough, Ultimate Taipan uses an interpolating SMT solver to obtain state assertions from...
  • Gridap

  • Referenced in 1 article [sw34982]
  • methods with Lagrangian, Raviart-Thomas, or Nédélec interpolations, and supports a wide range of problem ... detailed presentation of the mathematical abstractions behind the implementation of these FE methods). Gridap...
  • MauveDB

  • Referenced in 2 articles [sw28306]
  • store.In this paper we define a new abstraction called model-based views and present ... currently supports views based on regression and interpolation, using the Apache Derby open source DBMS...
  • ALBERT

  • Referenced in 81 articles [sw00025]
  • ALBERT - Software for scientific computations and applications. Adaptive...
  • BARON

  • Referenced in 311 articles [sw00066]
  • BARON is a computational system for solving nonconvex...
  • CGAL

  • Referenced in 355 articles [sw00118]
  • The goal of the CGAL Open Source Project...