Embedded Toolbox: Prove It! Proofs Start Where Static Analysis Stops

By Brandon Lewis


Embedded Computing Design

February 25, 2021


Embedded Toolbox: Prove It! Proofs Start Where Static Analysis Stops


Static analysis tools are widely used in safety- and security-critical applications as a means of finding and remediating coding errors. In fact, they are the de facto software testing tool in these industries.

Of course, static analysis is not the end-all, be-all of QA tools, nor is it a perfect solution by any stretch of the imagination. It is particularly adept at going through a codebase line-by-line and isolating potential errors, which are usually fairly simple, and providing a list of messages or alerts as to their possible cause. But there is another layer of analysis that can and often must be performed in order for developers to remediate bugs quickly and effectively.

And we're not talking about dynamic analysis. We're talking about proofs. When you need guarantees, rather than suggesting the possibility that they could exist and affect code operation in some way, proofs will prove that there aren't any errors. This can be applied to divide by zeros, buffer overflows, and a host of other bugs.

Building on a previous Embedded Toolbox where his colleague Rob Tice, used the CodePeer static analysis tool to address errors in the code of a Zumo robot, Yannick Moy, AdaCore's SPARK Product Manager, demonstrates how the SPARK language can be leveraged beyond static analysis to perform proofs natively during the software development process. This not only helps reach those elusive, extremely high double digit code coverage numbers, but also saves time and money on the backend.

Are you ready to prove how reliable your code is? Tune in and learn how.

TECH WAGER: If you find any bugs in the Github repo below, resolve them with SPARK proofs (tutorials and background information also available below), and screenshot/record your work, we will send you a FREE Zumo bot!

Brandon is responsible for guiding content strategy, editorial direction, and community engagement across the Embedded Computing Design ecosystem. A 10-year veteran of the electronics media industry, he enjoys covering topics ranging from development kits to cybersecurity and tech business models. Brandon received a BA in English Literature from Arizona State University, where he graduated cum laude. He can be reached at [email protected].

More from Brandon