I am a software engineer with a PhD in computer science. This site is mainly intended for notes and hints that I find useful for the daily work of a software engineer.
My PhD disseration was published by Springer Verlag and can be found on Amazon here:
"Algorithmic Differentiation of Pragma-Defined Parallel Regions: Differentiating Computer Programs Containing OpenMP"
Briefly, its topic is a correctness proof of a source code transformation. The source code transformation creates C code containing the code for calculating higher-order derivative values of a given function. The thesis examines how OpenMP pragmas inside the source file must be handled in the output of the transformation in order to keep correctness of the concurrent execution.
It turns out that in the case of tangent-linear transformation the transformation is relatively simple. In case of the adjoint source transformation with its inherit reverse of the data flow, the correctness proof was all but easy. Actually, it takes a couple of pages to handle all the possible cases.
The corresponding implementation of a source transformation tool called SPLc can be found on github.