This thesis presents MPI-Checker, a static analysis checker for MPI code written in C, based on Clang's Static Analyzer. The checker works with path-sensitive as well as with non-path-sensitive analysis which is purely based on information provided by the abstract syntax tree representation of source code. MPI-Checker's AST-based checks verify correct type usage in MPI functions, utilization of collective communication operations and provides experimental support to verify if point-to-point function calls have a matching partner. Its path-sensitive checks verify aspects of nonblocking communication, based on the usage of MPI requests, which are tracked by a symbolic representation of their memory region in the course of symbolic execution. The thesis elucidates for MPI-Checker relevant parts of the LLVM/Clang API and how the implementation is integrated into the architecture. Furthermore, the basics of MPI are explained. MPI-Checker introduces only negligible overhead on top of the Clang Static Analyzer core and is able to detect critical bugs in real world codebases, which is shown by evaluating analysis results for the open source projects AMG2013 and OpenFFT.

@misc{SCAOMSICWL15,
	author	 = {Alexander Droste},
	title	 = {{Static Code Analysis of MPI Schemas in C with LLVM}},
	advisors	 = {Michael Kuhn},
	year	 = {2015},
	month	 = {09},
	school	 = {Universität Hamburg},
	type	 = {Bachelor's Thesis},
	abstract	 = {This thesis presents MPI-Checker, a static analysis checker for MPI code written in C, based on Clang's Static Analyzer. The checker works with path-sensitive as well as with non-path-sensitive analysis which is purely based on information provided by the abstract syntax tree representation of source code. MPI-Checker's AST-based checks verify correct type usage in MPI functions, utilization of collective communication operations and provides experimental support to verify if point-to-point function calls have a matching partner. Its path-sensitive checks verify aspects of nonblocking communication, based on the usage of MPI requests, which are tracked by a symbolic representation of their memory region in the course of symbolic execution. The thesis elucidates for MPI-Checker relevant parts of the LLVM/Clang API and how the implementation is integrated into the architecture. Furthermore, the basics of MPI are explained. MPI-Checker introduces only negligible overhead on top of the Clang Static Analyzer core and is able to detect critical bugs in real world codebases, which is shown by evaluating analysis results for the open source projects AMG2013 and OpenFFT.},
}