Please use this identifier to cite or link to this item:
|Title:||Verification of programs with Z3|
|Department:||Computing and Software|
|Keywords:||Software Engineering;Software Engineering|
|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>|
|Appears in Collections:||Open Access Dissertations and Theses|
Items in MacSphere are protected by copyright, with all rights reserved, unless otherwise indicated.