How to Prove That Your C/C++ Code Is Safe and Secure

Are you afraid of finding critical software bugs too late? Would you like to obtain evidence that your code, either self-written or not, is free from overflow, divide-by-zero, out-of-bounds array access, and other run-time errors before you use it in safety- and security-critical systems? Do you need to comply with safety and security standards or guidelines like MISRA^®, SEI CERT-C, or ISO/IEC TS 17961?

In this paper, I discuss sophisticated static analysis methods that verify and prove the absence of run-time errors and vulnerabilities in the source code at unit and integration levels. By using sound formal methods that consider all potential inputs and control and data flows without code execution, organizations can gain confidence that the software they rely on is safe and secure. This approach gives organizations more than a mere error detection tool—it reduces testing and verification costs, and makes code quality transparent across entire teams.

This paper was presented at Embedded World Conference 2020.

Read full paper.