01whole.pdf (10.74 MB)
Download file

Generation and validation of witnesses to C programs

Download (10.74 MB)
posted on 28.03.2022, 13:41 by Mikeal Baric
Currently in society there is a combination of both simple and complex programs being developed, but they are not guaranteed to be bug free. There is a heavy reliance on testing a program's code in order to improve the code's quality. these testing methods, however, are time consuming and limited in scope, thus there is a need for new tools and technologies that can identify bugs in code, show an example of the bug and verify it. KLEE and KLOVER are two tools that have been developed to limit the likelihood of bugs and will be examined within this project. In this project we present our tool, Skink, and explore its processes to determine if a given C file is correct or not. We provide three examples of C files to see the expected test harness of our project. The objective of this project is to allow Skink to automatically generate an executable witness to prove the existence and verification of bugs within a given C file.


Table of Contents

1. Introduction -- 2. Background information -- 3. Background information of Skink -- 4. Skink project and its processes -- 5. Project implementation -- 6. Testing phase -- 7. Conclusions and future work -- 8. Abbreviations -- Appendices.


Bibliography: pages 45-46 Empirical thesis.

Awarding Institution

Macquarie University

Degree Type

Thesis bachelor honours


BSc (Hons), Macquarie University, Faculty of Science and Engineering, School of Engineering

Department, Centre or School

School of Engineering

Year of Award


Principal Supervisor

Franck Cassez


Copyright Mikeal Baric 2017. Copyright disclaimer: http://mq.edu.au/library/copyright




1 online resource (xv, 46 pages diagrams, tables)

Former Identifiers

mq:70385 http://hdl.handle.net/1959.14/1263236