Advertisement
Published in:
2010 | OriginalPaper | Chapter
URBiVA: Uniform Reduction to Bit-Vector Arithmetic
Authors : Filip Marić, Predrag Janičić
Published in: Automated Reasoning
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.