This is quite a bit more general than what your question directly asks, but take a look at "Spin," a "model checker" for concurrent systems. An online manual is here: http://spinroot.com/spin/Man/Manual.html
You will probably find it to be a bit "old school" in feel, but I see no reason why it wouldn't be suitable for the jobs you're interested in. Since it is quite general, however, you may need to do a bit of work to teach the tool about the problem space. The good news is that it is platform-independent. The bad news is you'd probably need to model each computer architecture explicitly (Spin doesn't intrinsically know about the guarantees of ARM vs. x86, for example). But maybe some of that work has been done elsewhere (I didn't check), and/or you could share pieces of what you do so others may benefit. The tool is open-source, after all.