BV2SMV

News

• 2013-04-12: Page is up. Currently this page is for reviewing only.

Overview

BV2SMV is a tool for translating a QF_BV formula in SMT2 format into an SMV specification.

Downloads

[ bv2smv-0.9.tar.gz ]

Evaluation

• benchmarking scripts
• generated benchmarks
• log files

All were used in experiments described in the following paper:

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, Finland, 2013.

Related Publications

• A. Fröhlich, G. Kovásznai, A. Biere. Efficiently Solving Bit-Vector Problems Using Model Checkers
• 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 appear).
• 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.

License