They didn't use the high-end static code analysis tools for C. This study was done by PolySync Technologies, so they have reason to leave real competition outside.<p>Run the same thing trough Astree. It can do static runtime error analysis based on abstract interpretation.<p>You can't prove that a program is free of all runtime errors (that is undecidable), but it's possible to signal all potential errors and that's what Astree does with as little wrong singals as possible.<p>Of course SPARK Ada is nice and I woudl prefer it, but in practice safety is not language dependent. It depends on the tools and methods.