Extending the KLEE test generator tool

OData support
Dr. Micskei Zoltán Imre
Department of Measurement and Information Systems

There are many methods to test software, most of which are supported by dedicated tools. One of the methods is the automatic generation of test inputs using symbolic execution, and a tool implementing it is the LLVM-based KLEE.

Its development started in 2007 as an academic prototype, then two years later it has been transformed into an open source project. Since then it is being used more and more widely as it becomes increasingly mature. However, it can not be described as fully production ready yet, since even its installation is a more complex task than usual. At the moment the recommended method of it is manual compilation from source, which is not particularly simple or user friendly.

In my thesis my goal is to improve this by creating easily installable and usable software packages for the Ubuntu operating system. In connection with this I show the general process of packaging this way, and also the details of the process performed in the specific case of KLEE (and its dependencies). This includes the downloading of the source code, its preparation for packaging, the generation of the source package, and its uploading into a PPA (personal package archive) on the Launchpad portal.

Then I describe the installation method of KLEE using the newly created packages -- which is much easier and faster now -- and its usage. I present the details of the tests performed on the tool installed this way on three different, Debian-based operating systems, and finally I mention the reception of the packages by the developers of the tool.


Please sign in to download the files of this thesis.