ABsolver - Arithmetic and Boolean solver

and

ABcircuit - Arithmetic and Boolean circuit library

Our framework provides a single engine to possibly solve all mixed arithmetic and Boolean problems using standard tools, such as zChaff or COIN. Even though the primary intend was to tackle linear arithmetic, the extensible architecture proved useful as we added non-linear solvers as well and are thus able to solve a set of mixed Boolean and non-linear problems too, which, to the best of our knowledge, no other tool is capable of. Furthermore a layered design approach makes it easy to add new solvers and thus new problem domains, and will also help new programmers joining in.

The command line interface allows for customization of the background solvers, whereby heuristics are supported which should help to solve even very hard problems.

Download ABsolver

A set of benchmarks and their results can be found here.

Publications

Andreas Bauer, Martin Leucker, Christian Schallhart, and Michael Tautschnig. Don't care in SMT---Building flexible yet efficient abstraction/refinement solvers. International Journal on Software Tools for Technology Transfer, 2008. Accepted for publication.

Andreas Bauer, Martin Leucker, Christian Schallhart, and Michael Tautschnig. Don't care in SMT---Building flexible yet efficient abstraction/refinement solvers. In Proceedings of the 2007 ISoLA Workshop On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), Poitiers, France, pages 135-146, December 2007.

Andreas Bauer, Markus Pister, and Michael Tautschnig. Tool-support for the analysis of hybrid systems and models. In Proceedings of the 2007 Conference on Design, Automation and Test in Europe (DATE), Nice, France, pages 924-929, April 2007. European Design and Automation Association.

$Date: 2009-10-19 22:44:59 +0200 (Mon, 19 Oct 2009) $