Universität Bremen  
  Universität Bremen FB3 TZI BISS  
  AG BS > > Deutsch
English
 

SONOLAR
 
SONOLAR, the Solver for non-linear Arithmetic, is an SMT-Solver that solves quantifier-free fixed-size bit-vector logic formulas.
The solver supports the SMT-LIB format including the following logics:
  • Bit vectors (QF_BV).
  • Bit vectors with arrays (QF_ABV).
  • IEEE 754 floating point operations including all rounding modes with arbitrary range and precision:
    The solver supports the symbols described in the SMT-LIB theory for floting point numbers. Since SMT-LIB logic names are yet to be defined for this theory, the logics QF_BV and QF_ABV have been extended by these symbols.
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 [2] 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 and Glucose 3.0 are used as SAT solvers [4, 1].

SONOLAR is currently used for automatic test data generation in the field of model-based testing and C/C++-unit testing [6, 7, 8, 3, 5].

Contact

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

Downloads

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

References

[1] Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern sat solvers. In Proceedings of the 21st International Jont Conference on Artifical Intelligence, IJCAI'09, pages 399-404, San Francisco, CA, USA, 2009. Morgan Kaufmann Publishers Inc.
[2] 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.
[3] Gustavo Carvalho, Flávia de Almeida Barros, Florian Lapschies, Uwe Schulze, and Jan Peleska. Model-based testing from controlled natural language requirements. In FTSCS, pages 19-35, 2013.
[4] Niklas Eén and Niklas Sörensson. An Extensible SAT-solver. In SAT, pages 502-518, 2003.
[5] Tatiana Mangels and Jan Peleska. Ctgen - a unit test generator for c. In SSV, pages 88-102, 2012.
[6] 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.
[7] 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/.
[8] Jan Peleska, Artur Honisch, Florian Lapschies, Helge Löding, Hermann Schmid, Peer Smuda, Elena Vorobev, and Cornelia Zahlten. A Real-World Benchmark Model for Testing Concurrent Real-Time Systems in the Automotive Domain. In Burkhart Wolff and Fatiha Zaidi, editors, Testing Software and Systems. Proceedings of the 23rd IFIP WG 6.1 International Conference, ICTSS 2011, volume 7019 of LNCS, pages 146-161, Heidelberg Dordrecht London New York, November 2011. IFIP WG 6.1, Springer.
 
   
Author: florian 		 
  AG BS 
Last updated: November 2, 2022   Impressum