Просмотр исходного текста страницы Применение SMT-солверов в статическом и динамическом символьном выполнении — экспериментальное исследование (Никита Малышев, ISPRASOPEN-2019)

;{{SpeakerInfo}}: {{Speaker|Никита Малышев}}
<blockquote>
В этой статье рассматриваются различные характеристики и аспекты работы с SMT-решателями при обработке формул, полученных во время чувствительного к путям статического анализа и динамического символьного выполнения. Рассматриваются общие закономерности построения SMT формул в логике QF_BV во время анализа и особенности их обработки. Также произведено сравнение различных решателей по двум наборам запросов, полученных статическим анализатором Svace и инструментом динамического символьного выполнения Anxiety. Поверхностная попытка создания портфолио решателей на основе машинного обучения показала, что время решения может быть немного улучшено, но техническая реализация и грамотная работа с признаками могут быть слишком сложны. 

----

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 nonincremental. Moreover, the more queries we solve incrementally, the higher acceleration we get.
</blockquote>

{{VideoSection}}
{{vimeoembed|378874241|800|450}}
{{youtubelink|5_2fDPTUh-s}}
{{letscomment}}

{{SlidesSection}}
[[File:Применение SMT-солверов в статическом и динамическом символьном выполнении — экспериментальное исследование.pdf|left|page=-|300px]]

{{----}}
[[File:{{#setmainimage:Применение SMT-солверов в статическом и динамическом символьном выполнении — экспериментальное исследование!.jpg}}|center|640px]]
{{LinksSection}}
<!-- * [ Talks page on site] -->
<!-- <blockquote>[©]</blockquote> -->

{{fblink|2473983572854649}}                                          
{{vklink|1509}}                                          
<references/>

<!-- topub -->

{{stats|disqus_comments=0|refresh_time=2021-08-31T17:59:57.242678|vimeo_plays=9|youtube_comments=0|youtube_plays=42}}

[[Категория:ISPRASOPEN-2019]]
[[Категория:Верификация]]