Verification of programs with Z3

Abstract

<p>Fixing the errors in programs is usually very labor-intensive and thus an expensive task. It is also known to be prone to human error thus not fully reliable. There have been many methods of program verification developed, however they still require a lot of human input and interaction throughout the process. There is an increasing need for an automated software verification tool that would reduce human interaction to the minimum. Satisfiability Modulo Theories (SMT) solvers, a series of SAT-solvers such as Z3 looked initially to be a proper and easy to use tool. Its syntax is fairly uncomplicated and it seems to be quite efficient. In this thesis, Z3 is used to find loop invariants, prove some properties of concurrent programs written in Owicki-Gries style and prove some properties of recursive programs. It appears that - in general- Z3 does not work as well as expected in all areas to which it was applied.</p>