URBiVA: uniform reduction to bit-vector arithmetic

DOI10.1007/978-3-642-14203-1_29MaRDI QIDQ5747772zbMATH OpenOpenAlexFDO

Authors Filip Marić, Predrag Janičić

Publication date 14 September 2010

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14203-1_29

Mathematics Subject Classification ID

Recommendations

• URSA: a system for uniform reduction to SAT
• An alternative to SAT-based approaches for bit-vectors
• Deciding Bit-Vector Arithmetic with Abstraction
• A bit-vector solver with word-level propagation
• Wombit: a portfolio bit-vector solver using word-level propagation

Cites work

• Deciding Bit-Vector Arithmetic with Abstraction
• Formalization and implementation of modern SAT solvers
• URBiVA: uniform reduction to bit-vector arithmetic

Cited in

(5)

• meSAT: multiple encodings of CSP to SAT
• Extending SMT solvers with support for finite domain \texttt{alldifferent} constraint
• Synthesis for Unbounded Bit-Vector Arithmetic
• URSA: a system for uniform reduction to SAT
• URBiVA: uniform reduction to bit-vector arithmetic

Describes a project that uses

Uses Software

• URBiVA
• MathSAT
• Boolector
• Yices

This page was built for publication: URBiVA: uniform reduction to bit-vector arithmetic

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