Abstract
This paper studies the performance and working aspects of SMT solvers on processing formulas acquired during path-sensitive static analysis and dynamic symbolic execution. We review some general patterns of building SMT formulas in the QF_BV logic during analysis and related technical specifics. We also provide the results of comparing different solvers on two sets of requests obtained by Svace static analyzer and Anxiety dynamic symbolic execution tool. It turns out that Yices2 solver performs the best, although, for Svace, notable part of requests can be done better by other solvers. In return, Yices2 misses some features crucial to top-tier analyzers such as deterministic time limit. A brief attempt at making machine learning based solver portfolio shows that solving time can be enhanced, but requires some serious work on feature selection, while technical difficulties may render it unpractical. For Anxiety we found out that with Yices2 incremental solving is almost always faster (sometimes dozens of times faster) than non-incremental. Moreover, the more queries we solve incrementally, the higher acceleration we get.
Original language | English |
---|---|
Title of host publication | Proceedings of the 2019 Ivannikov Ispras Open Conference (ISPRAS) |
Editors | Sergei Prokhorov |
Publisher | Institute of Electrical and Electronics Engineers |
Pages | 9-15 |
Number of pages | 7 |
ISBN (Electronic) | 978-1-7281-6055-9 |
ISBN (Print) | 978-1-7281-6056-6 |
DOIs | |
Publication status | Published - 14 Feb 2020 |
Event | The Ivannikov ISP RAS Open Conference, 2019 - Moscow, Russian Federation Duration: 5 Dec 2019 → 6 Dec 2019 https://www.isprasopen.ru/2019/en/ |
Conference
Conference | The Ivannikov ISP RAS Open Conference, 2019 |
---|---|
Country/Territory | Russian Federation |
City | Moscow |
Period | 5/12/19 → 6/12/19 |
Internet address |
Keywords / Materials (for Non-textual outputs)
- symbolic execution
- static analysis
- SMT solvers
- QF_BV
- solver portfolio