bv2epr: a tool for polynomially translating quantifier-free bit-vector formulas into EPR

DOI10.1007/978-3-642-38574-2_32MaRDI QIDQ4928459zbMATH OpenOpenAlexFDO

Authors Gergely Kovásznai, Andreas Fröhlich, Armin Biere

Publication date 14 June 2013

Published in Automated Deduction – CADE-24 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-38574-2_32

Mathematics Subject Classification ID

Recommendations

• Efficiently solving quantified bit-vector formulas
• More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding
• Solving quantified bit-vector formulas using binary decision diagrams
• Complexity of fixed-size bit-vector logics
• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic

Cited in

(4)

• More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• bv2epr
• Complexity of fixed-size bit-vector logics

Describes a project that uses

Uses Software

• SMT-LIB

This page was built for publication: bv2epr: a tool for polynomially translating quantifier-free bit-vector formulas into EPR

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4928459)