Research group

Verification or Program Analysis Lab

On application of SMT-solvers for software analysis

12 December 2016

A lot of techniques in modern software analysis is almost impossible to implement without the use of SMT solvers. Despite the rapid progress in SMT theory, its use in practice is often hindered by different obvious and not-so-much problems. In this talk we will discuss what SMT solvers actually are (and, more importantly, what they are not), what they can and cannot do, how one can use them for her specific needs and what are the challenges of making them actually work in practice.

Presenter: Mikhail Belyaev, Peter the Great SPbPU