,
9 tweets,
1 min read
Read on Twitter
In my humble few months verifying safety critical code in industry, I now wish I knew quite a few things during my PhD:
A criticism I often received was that our tool (T2), needed to go beyond verifying C. C was simple, archaic, unsafe, and no longer used.
Work towards higher level functions, they said. It's the future, they said. Boy, do I have a surprise for you.
In A LOT of safety critical code, C IS KING. Nuclear, aviation, rail, automotive, you name it. And not because it's legacy.
C works WELL for these systems. I now wish I had read the C standard forwards and backwards, knew all variations of it, and nuances.
Not only so, a huge part of the verification community has concentrated their efforts on being LLVM compatible. This is convenient and all..
Yet very little of the safety critical industry uses GCC, let alone LLVM. Many manufacturers have their own (and often verified) compiler.
Making new verification tools absolutely incompatible with these systems.
I hope those of you working on C verification know that your efforts are well appreciated in industry, and that C is not dead.
