
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 addmultiply circuits, and dividebyconstant 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 bitvectors...

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...

CXSC
 Referenced in 110 articles
[sw00181]
 CXSC. A programming environment for verified scientific...

CXSC 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...