- 2013-04-12: Page is up. Currently this page is for reviewing
BV2SMV is a tool for translating a QF_BV formula in SMT2 format
into an SMV specification.
[ bv2smv-0.9.tar.gz ]
All were used in experiments described in the following
Andreas Fröhlich, Gergely Kovásznai, Armin Biere. Efficiently
Solving Bit-Vector Problems Using Model Checkers. In Proc. 11th
Intl. Workshop on Satisfiability Modulo Theories
(SMT'13), pages 6-15, aff. to SAT'13, Helsinki,
- A. Fröhlich, G. Kovásznai, A. Biere. Efficiently Solving Bit-Vector Problems Using
- G. Kovásznai, A. Fröhlich, A. Biere. BV2EPR: A Tool for Polynomially Translating
Quantifier-free Bit-Vector Formulas into EPR. In
Proc. 24th Intl. Conference on Automated
Deduction (CADE-24), Lake Placid, New York, US, 2013 (to
- A. Fröhlich, G. Kovásznai, A. Biere. More on the Complexity of Quantifier-Free
Fixed-Size Bit-Vector Logics with Binary Encoding In Proc.
15th Intl. Computer Science Symposium in Russia (CSR'13),
Ekaterinburg, Russia, 2013 (to appear).
- G. Kovásznai, A. Fröhlich, A. Biere. On the Complexity of Fixed-Size Bit-Vector
Logics with Binary Encoded Bit-Width. In
Proc. 10th Intl. Workshop on Satisfiability
Modulo Theories (SMT'12), pages 44-55, aff. to IJCAR'12,
Manchester, UK, 2012.
BV2SMV is copyrighted 2013 by Andreas Fröhlich and Gergely
Kovásznai, Institute for Formal Models and Verification, Johannes
Kepler University, Linz, Austria, under the GNU General Public
License Version 3 (GPLV3). You can find more information about
GPLV3 in the file COPYING that comes with the sources.