Boolector

E904161
SMT solver decision procedure software tool

Boolector is an efficient SMT solver specialized in bit-vectors, arrays, and uninterpreted functions, widely used in formal verification and model checking.

Try in SPARQL Jump to: Statements Referenced by

Statements (47)

Predicate Object
instanceOf SMT solver ⓘ
decision procedure ⓘ
software tool ⓘ
category formal methods tool ⓘ
developedAt Johannes Kepler University Linz NERFINISHED ⓘ
focusesOn quantifier-free bit-vector logics ⓘ
hasAuthor Armin Biere NERFINISHED ⓘ
hasFeature assumption-based solving ⓘ
bit-blasting ⓘ
incremental solving ⓘ
model generation ⓘ
rewriting-based simplification ⓘ
unsat core extraction ⓘ
hasInputFormat SMT-LIB v2 NERFINISHED ⓘ
hasInterface C API NERFINISHED ⓘ
command-line interface ⓘ
hasNameOrigin portmanteau of "boo" and "vector" (bit-vector) ⓘ
isOpenSource true ⓘ
license MIT License ⓘ
optimizedFor bit-vector performance ⓘ
efficiency ⓘ
participatedIn SMT-COMP NERFINISHED ⓘ
specializedIn arrays ⓘ
bit-vectors ⓘ
uninterpreted functions ⓘ
supportsLogic arrays ⓘ
bit-vectors ⓘ
uninterpreted functions ⓘ
supportsOperation model extraction ⓘ
proof-based analysis ⓘ
satisfiability checking ⓘ
supportsQuantifiers limited GENERATED ⓘ
supportsSMTLIBLogic QF_ABV GENERATED ⓘ
QF_AUFBV GENERATED ⓘ
QF_BV GENERATED ⓘ
QF_UFBV GENERATED ⓘ
supportsStandard SMT-LIB NERFINISHED ⓘ
supportsTheory theory of arrays ⓘ
theory of fixed-size bit-vectors ⓘ
theory of uninterpreted functions ⓘ
usedFor formal verification ⓘ
hardware verification ⓘ
model checking ⓘ
software verification ⓘ
usedInDomain hardware model checking ⓘ
software model checking ⓘ
writtenInLanguage C ⓘ

Referenced by (1)

Full triples — surface form annotated when it differs from this entity's canonical label.

Satisfiability Modulo Theories (SMT) → hasSolver → Boolector ⓘ
subject surface form: Satisfiability Modulo Theories