SMT Solvers in Application to Static and Dynamic Symbolic Execution: A Case Study

Nikita Malyshev, Irina Dudina, Daniil Kutz, Alexander Novikov, Sergey Vartanov

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish
Title of host publicationProceedings of the 2019 Ivannikov Ispras Open Conference (ISPRAS)
EditorsSergei Prokhorov
PublisherInstitute of Electrical and Electronics Engineers
Pages9-15
Number of pages7
ISBN (Electronic)978-1-7281-6055-9
ISBN (Print)978-1-7281-6056-6
DOIs
Publication statusPublished - 14 Feb 2020
EventThe Ivannikov ISP RAS Open Conference, 2019 - Moscow, Russian Federation
Duration: 5 Dec 20196 Dec 2019
https://www.isprasopen.ru/2019/en/

Conference

ConferenceThe Ivannikov ISP RAS Open Conference, 2019
Country/TerritoryRussian Federation
CityMoscow
Period5/12/196/12/19
Internet address

Keywords / Materials (for Non-textual outputs)

  • symbolic execution
  • static analysis
  • SMT solvers
  • QF_BV
  • solver portfolio

Fingerprint

Dive into the research topics of 'SMT Solvers in Application to Static and Dynamic Symbolic Execution: A Case Study'. Together they form a unique fingerprint.

Cite this