3 ms·
SPARK is based on Ada. Astree also seems to be limited only to C. Chrome, to the opposite, is written in millions of lines of C++.
by wolfgke 11y ago
SPARK is based on Ada. Astree also seems to be limited only to C. Chrome, to the opposite, is written in millions of lines of C++.
- nickpsecurity 11y agoThe reason I mentioned SPARK and Astree is because they're excellent at what they do. People Googling them will understand how these approaches work to prove absence of bugs rather than test for their presence. Then, they might experiment with some of the others on the list. I mentioned PolySpace as an example of something more appropriate for Chrome because it supports C++ and is used in high integrity applications.