SONOLAR

by Florian Lapschies (florian@informatik.uni-bremen.de)

SONOLAR, the Solver for non-linear Arithmetic, is an SMT-Solver that solves quantifier-free fixed-size bit-vector logic formulas.
It currently supports the following:

All symbols of the SMT-LIB logic QF_BV.
All symbols of the SMT-LIB logic QF_ABV.
Overflow predicates for integral arithmetic.
IEEE 754 floating point operations including all rounding modes with arbitrary range and precision.

SONOLAR uses bit-blasting to translate bitvector constraints to a Boolean formula and lets a SAT solver decide the satisfiability. For handling the extensional theory of arrays, the lemmas on demand approach described in [3] has been adopted. To this end a series of word-level simplification rules are applied to the input formula which is then converted to an And-Inverter Graph. After performing bit-level simplifications a Boolean CNF formula is generated and fed to a SAT solver. MiniSat 2.2.0 is used as the default SAT solver [6].

SONOLAR is currently used for automatic test data generation in the field of model-based testing and C/C++-unit testing [1, 2, 4, 5].

Downloads

The downloads include static and shared libraries of SONOLAR as well as C++ header-files.

In addition, SONOLAR can be used as a standalone program reading formulas in SMT-LIB format version 1.2 and 2.0.

References

[1]	Jan Peleska. Integrated and Automated Abstract Interpretation, Verification and Testing of C/C++ Modules. In D. Dams, U. Hannemann, and M. Steffen, editors, Concurrency, Compositionality and Correctness. Essays in Honor of Willem-Paul de Roever, volume 5930 of LNCS, pages 277-299. Springer, 2010.
[2]	Jan Peleska. A Unified Approach to Abstract Interpretation, Formal Verification and Testing of C/C++ Modules. In John S. Fitzgerald, Anne E. Haxthausen, and Husnu Yenigun, editors, Theoretical Aspects of Computing - ICTAC 2008, 5th International Colloquium, volume 5160 of LNCS, pages 3-22, Istanbul, September 2008. Springer.
[3]	Robert Brummayer and Armin Biere. Lemmas on Demand for the Extensional Theory of Arrays. In Proc. 6th Intl. Workshop on Satisfiability Modulo Theories (SMT'08), New York, NY, USA, 2008. ACM.
[4]	Jan Peleska, Elena Vorobev, and Florian Lapschies. Automated Test Case Generation with SMT-Solving and Abstract Interpretation. In Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors, Nasa Formal Methods, Third International Symposium, NFM 2011, volume 6617 of LNCS, pages 298-312, Pasadena, CA, USA, April 2011. Springer.
[5]	Jan Peleska, Florian Lapschies, Helge Löding, Peer Smuda, Hermann Schmid, Elena Vorobev, and Cornelia Zahlten. Embedded Systems Testing Benchmark, 2011. http://www.informatik.uni-bremen.de/agbs/testingbenchmarks/.
[6]	Niklas Eén and Niklas Sörensson. An Extensible SAT-solver. In SAT, pages 502-518, 2003.