URBiVA: Uniform Reduction to Bit-Vector Arithmetic

DOI10.1007/978-3-642-14203-1_29zbMath1291.68361OpenAlexW1491554327MaRDI QIDQ5747772

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

Related Items (3)

Extending SMT solvers with support for finite domain \texttt{alldifferent} constraint ⋮ URBiVA: Uniform Reduction to Bit-Vector Arithmetic ⋮ meSAT: multiple encodings of CSP to SAT

Uses Software

• Boolector
• Yices
• URBiVA
• MathSAT

Cites Work

• Formalization and implementation of modern SAT solvers
• URBiVA: Uniform Reduction to Bit-Vector Arithmetic
• Deciding Bit-Vector Arithmetic with Abstraction

This page was built for publication: URBiVA: Uniform Reduction to Bit-Vector Arithmetic