Also see the work done in the under-utilized K Framework which captures & rejects undefined behavior as well:

http://fsl.cs.illinois.edu/index.php/Defining_the_Undefinedn...

Since it's K, they were able to turn it into a GCC-like compiler for you verifying things about your application. If it even compiles, you have no undefined behavior.

https://github.com/kframework/c-semantics

On concurrency side, it's built on top of Maude tool that an inexperienced student was able to use to find errors in Eiffel's SCOOP model for concurrency. So, it can probably handle that aspect as well.