[KsassPeuk]

Note that most Frama-C analysis are not debugging tools. Although you can find bugs with them, they mostly focus on proving that there are no bugs, which is slightly different.

There are plugins for multi-thread programs.

One is an experimental plugin called Conc2Seq that I developed during my thesis with a focus on proving properties about small modules with a few functions accessing concurrently some global resources. Note however hat it is very experimental and it is not actively developed anymore, but at least it can be updated or give some ideas on how to write such an analyzer.

The second is a proprietary plugin called MThread (base on the Eva analysis of Frama-C), but it is only available via licensing.