URBiVA: uniform reduction to bit-vector arithmetic. We describe a system URBiVA for specifying and solving a range of problems by uniformly reducing them to bit-vector arithmetic (bva). A problem description is given in a C-like specification language and this high-level specification is transformed to a bva formula by symbolic execution. The formula is passed to a bva solver and, if it is satisfiable, its models give solutions of the problem. The system can be used for efficient modelling (specifying and solving) of a wide class of problems. Several state-of-the-art solvers for bva are currently used (Boolector, MathSAT, Yices) and additional solvers can be easily included. Hence, the system can be used not only as a specification and solving tool, but also as a platform for evaluation and comparison between bva solvers.
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Stojadinović, Mirko; Marić, Filip: meSAT: multiple encodings of CSP to SAT (2014)
- Janičić, Predrag: URSA: a system for uniform reduction to SAT (2012)
- Marić, Filip; Janičić, Predrag: URBiVA: uniform reduction to bit-vector arithmetic (2010)