In mathematical logic and computability theory, Beaver is a Satisfiability Modulo Theories (SMT) decision procedure for the theory of quantifier-free finite-precision bit-vector arithmetic. Its prototype implementation supports all operators defined under QF_BV, including signed and unsigned non-linear arithmetic operators.
| Property | Value |
|---|
| dbpprop:abstract
|
- In mathematical logic and computability theory, Beaver is a Satisfiability Modulo Theories (SMT) decision procedure for the theory of quantifier-free finite-precision bit-vector arithmetic. Its prototype implementation supports all operators defined under QF_BV, including signed and unsigned non-linear arithmetic operators. Beaver is specially adapted for solving SMT formulae arising out of program analysis (rich in conjunction of linear constraints such as path feasibility queries), computer security (rich in nonlinear arithmetic) and formal equivalence checking (rich Boolean structure).
|
| dbpprop:reference
| |
| rdfs:comment
|
- In mathematical logic and computability theory, Beaver is a Satisfiability Modulo Theories (SMT) decision procedure for the theory of quantifier-free finite-precision bit-vector arithmetic. Its prototype implementation supports all operators defined under QF_BV, including signed and unsigned non-linear arithmetic operators.
|
| rdfs:label
|
- Beaver bit-vector decision procedure
|
| skos:subject
| |
| foaf:page
| |
| is dbpprop:disambiguates
of | |
| is dbpprop:redirect
of | |
![[RDF Data]](/statics/sw-cube.png)
