http://spinroot.com/gerard/pdf/P10.pdf (some are more/less appropriate for non-embedded-systems)

In general, the answer typically involves formal specification and formal methods that check the code against these specifications, combined with testing and coding standards that result in analysable code.

More references:

https://www.cs.umd.edu/~mvz/cmsc630/clarke96formal.pdf

http://research.microsoft.com/en-us/um/people/lamport/tla/fo...

You might want to look into coding standards for C and special languages like Ada (like C, but less writeable, more readable with strong types) and Esterel (deterministic multithread scheduling). Seriously, Esterel is probably the coolest thing you'll read about this week.

There's also various specification languages for multithreaded behaviour, which allows you to analyse your programs behaviour using software tools, for example SPIN[0].

0: http://en.wikipedia.org/wiki/SPIN_model_checker

Search for high integrity software.

For example, with MISRA it may be C, but feels like Ada.

http://www.misra.org.uk/

Or Spark similarly for Ada

http://www.spark-2014.org/