3 ms·
>The JPL recommended static analyzers are fast, and produce sparse and accurate messages. I'm interested in what analyzers they may be recommending. I think th
by technion 11y ago
>The JPL recommended static analyzers are fast, and produce sparse and accurate messages.
I'm interested in what analyzers they may be recommending. I think this is a field that's come a long way since 2009.
A lot of these standards could actually be implemented as rules in modern products, which would assist with using them.
- mturmon 11y agoThe lead author of this standard is Gerard Holzmann, a Fellow of the ACM and a member of the NAE. He works at JPL, and has been instrumental in introducing code analysis to flight software (e.g., http://lars-lab.jpl.nasa.gov http://lars-lab.jpl.nasa.gov). The analyzers JPL currently uses are Coverity, Semmle, CodeSonar, and Klocwork. Coverity seems most common. Of course, Gerard was an author of Spin (http://spinroot.com/spin/whatispin.html http://spinroot.com/spin/whatispin.html).