The 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).
The analyzers JPL currently uses are Coverity, Semmle, CodeSonar, and Klocwork. Coverity seems most common.
Comments
The 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).
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).