• petBoss

  • Referenced in 1 article [sw29334]
  • circuit verification. The paper describes a practical software tool for the verification of integer arithmetic ... polynomial. The verification uses an algebraic model of the circuit and is accomplished by rewriting ... enable extraction of the essential arithmetic components of the circuit. The tool is integrated with ... fused add-multiply circuits, and divide-by-constant circuits. The entire verification system is offered...
  • JBernstein

  • Referenced in 2 articles [sw19486]
  • nonlinear real arithmetic constraints is essential in many automated verification and synthesis tasks for hybrid ... processors, and mixed analog/digital circuits. Despite substantial advances in verification technology, complexity issues with classical ... decision procedures for nonlinear real arithmetic are still a major obstacle for formal verification...
  • RevSCA

  • Referenced in 2 articles [sw37909]
  • have shown very good results in verification of integer multipliers. The success is based ... identifying the atomic blocks of the arithmetic circuits using dedicated reverse engineering techniques. Our approach ... confirm the efficiency of our approach in verification of a wide variety of integer multipliers...
  • Beaver

  • Referenced in 10 articles [sw00071]
  • Beaver: Engineering an efficient SMT solver for bit...
  • Boolector

  • Referenced in 31 articles [sw00085]
  • Boolector: an efficient SMT solver for bit-vectors...
  • cdd

  • Referenced in 115 articles [sw00114]
  • The program cdd+ (cdd, respectively) is a C...
  • CoCoA

  • Referenced in 654 articles [sw00143]
  • CoCoA is a system for Computations in Commutative...
  • Coq

  • Referenced in 1880 articles [sw00161]
  • Coq is a formal proof management system. It...
  • C-XSC

  • Referenced in 110 articles [sw00181]
  • C-XSC. A programming environment for verified scientific...
  • C-XSC 2.0

  • Referenced in 127 articles [sw00182]
  • A C++ class library for extended scientific computing...
  • GAP

  • Referenced in 3154 articles [sw00320]
  • GAP is a system for computational discrete algebra...
  • INTBIS

  • Referenced in 31 articles [sw00442]
  • Algorithm 681: INTBIS, a portable interval Newton/bisection package...
  • Isabelle

  • Referenced in 698 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • LAPACK

  • Referenced in 1695 articles [sw00503]
  • LAPACK is written in Fortran 90 and provides...
  • LEDA

  • Referenced in 263 articles [sw00509]
  • In the core computer science areas -- data structures...
  • LSQR

  • Referenced in 394 articles [sw00530]
  • Algorithm 583: LSQR: Sparse Linear Equations and Least...
  • Macaulay2

  • Referenced in 1904 articles [sw00537]
  • Macaulay2 is a software system devoted to supporting...
  • Magma

  • Referenced in 3296 articles [sw00540]
  • Computer algebra system (CAS). Magma is a large...
  • Maple

  • Referenced in 5363 articles [sw00545]
  • The result of over 30 years of cutting...
  • Mathematica

  • Referenced in 6337 articles [sw00554]
  • Almost any workflow involves computing results, and that...