Abstract

We present OL1V3R, a solver for the SMT floating-point theory that is based on stochastic local search (SLS). We adapt for OL1V3R the key ingredients of related work on leveraging SLS to solve the SMT fixed-sized bit-vector theory, and confirm its effectiveness by comparing it with mature solvers. Finally, we discuss the limitations of OL1V3R and propose solutions to make it more powerful.

Citation

Shaobo He, Marek Baranowski, Zvonimir Rakamaric
Stochastic Local Search for Solving Floating-Point Constraints
Proceedings of the 12th International Workshop on Numerical Software Verification (NSV), 11652: 76--84, doi:10.1007/978-3-030-28423-7_5, 2019.

BibTeX

@inproceedings{2019_nsv_hbr,
  title = {Stochastic Local Search for Solving Floating-Point Constraints},
  author = {Shaobo He and Marek Baranowski and Zvonimir Rakamaric},
  booktitle = {Proceedings of the 12th International Workshop on Numerical Software Verification (NSV)},
  series = {Lecture Notes in Computer Science},
  volume = {11652},
  publisher = {Springer},
  editor = {Majid Zamani and Damien Zufferey},
  pages = {76--84},
  doi = {10.1007/978-3-030-28423-7_5},
  year = {2019}
}

Acknowledgements

Supported in part by the National Science Foundation (NSF) awards CCF 1552975 and CCF 1704715.

Abstract

Citation

BibTeX

Acknowledgements

Resources