01whole.pdf (17.77 MB)
Download file

Verification of multi-threaded C programs

Download (17.77 MB)
thesis
posted on 28.03.2022, 17:06 authored by Matthew Pigram
Verifying the correctness of a program involves providing a guarantee, in the form of a logical proof, that the program is free of bugs for all possible inputs. It is therefore able to provide software developers and users with a much higher degree of confidence in a program's ability to perform its job than traditional testing, due to the fact that it produces certainty rather than empirical evidence of a program's partial correctness, something which is especially important when that program is responsible for large sums of money or human lives. Multi-threaded programs are able to take advantage of modern multi-core architectures more effectively than single-threaded programs but introduce challenges both to the author and the verifier. Concurrent programs are regarded as being more difficult to write and understand than traditional sequential programs by developers due to the large number of ways in which the multiple threads may interact throughout a program's execution. As such, the ability to formally verify this type of software is perhaps even more valuable than traditional single-threaded programs. For verification, the combinatorial number of ways in which the operations of each thread may be interleaved by a non-deterministic scheduler introduces the problem of state-space explosion. Here, we describe a method for adapting trace abstraction refinement, an existing technique for verification of single-threaded programs for application to multi-threaded programs in combination with an approach to reduce the state space of the program based on dynamic partial order reduction. We apply this method to enable the verification of C programs, building on the work on this topic by Cassez and Zeigler.

History

Table of Contents

1. Introduction -- 2. Background and related work -- 3. From C programs to formal automata based abstraction -- 4. Implementation -- 5. Results -- 6. Conclusions -- 7. Future work -- 8. Abbreviations -- Bibliography -- Appendices.

Notes

Empirical thesis. Bibliography: pages 61-63

Awarding Institution

Macquarie University

Degree Type

Thesis bachelor honours

Degree

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

Department, Centre or School

School of Engineering

Year of Award

2016

Principal Supervisor

Franck Cassez

Additional Supervisor 1

Anthony Sloane

Rights

Copyright Matthew Pigram 2016. Copyright disclaimer: http://mq.edu.au/library/copyright

Language

English

Extent

1 online resource (xi, 76 pages diagrams, graphs, tables)

Former Identifiers

mq:70361 http://hdl.handle.net/1959.14/1262996

Usage metrics

Keywords

Exports