The winter of 2014 was cold.

During the months of January and February of the year 2014 I gave an objective to myself. It was to finish the masters dissertation to the point of submission. I also learned that picking a hard topic was probably not the best idea but it was certainly rewarding. Nonetheless, I still received a distinction (the Oxford version of an A) for the work. So, I'm happy share it with the world welcoming any sort of feedback.

If you're interested you can read the full paper here: The full paper

Abstract

Personal computing devices and servers are becoming more powerful by the day through hardware parallelisation. Such advances require developers to look into concurrency in order to take advantage of the new computing power. However, much of the code is written without formal verification and checked only heuristically through unit or other tests. This dissertation will show how Communicating Sequential Processes (CSP) can be used to detect errors in an application that supports concurrent execution. This is done by isolating common concurrency problems and mapping them into CSP representations. Finally, Failures-Divergences Refinement (FDR) software package is used to perform refinement checks to detect the errors in the source code. This process allows the developer to build assertions that their code must pass to prove its correctness. 

Acknowledgements
I would like to thank my advisor, Dr. Andrew Simpson, and the Software Engineering Program staff for their guidance and quick responses. This project could not have been accomplished without the generosity, patience and accommodation of the family scholarship fund. I am particularly grateful to the American people for providing the opportunity and the Lithuanian people for their infinitely delicious food and heavenly honey. Finally, I wish to thank my wife, Diana, for her love, support and conversation.