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

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

License

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.