A few summers ago I was an intern at JPL working on a static analysis suite for this exact standard. Writing code checkers for these sorts of rules is a really

A few summers ago I was an intern at JPL working on a static analysis suite for this exact standard. Writing code checkers for these sorts of rules is a really interesting exercise and it helped me grow a lot as a programmer! I went from having no exposure to formal languages, parsing, and grammars to actively playing around with these concepts to try and help build more reliable software. It was a humbling, challenging, and incredibly rewarding experience. Sometimes, a rule is extremely simple to implement. For example, checking a rule that requires that an assert is raised after every so many lines within a given scope is just a matter of picking the right sed expression. Other times, you really need an AST to be able to do anything at all. A rule like "In compound expressions with multiple sub-expressions the intended order of evaluation shall be made explicit with parentheses" is particularly challenging. I spent a few weeks on this rule! I was banging my head, trying to learn the fundamentals of parsing languages, spending my hours diving into wikipedia articles and learning lex and yacc. The grad students at LaRS were always extremely helpful and were always willing to help tutor me and teach me what I needed to learn (hi mihai and cheng if you're reading!). After consulting them and scratching our heads for a while, we figured we might be able to do it with a shift-reduce parser when a shift or reduce ambiguity is introduced during the course of parsing a source code file. This proved beyond the scope of what I'd be able to do within an internship, but it helped me appreciate the nuance and complexity hidden within even seemingly simple statements about language properties. Automated analysis of these rules gives you a really good appreciation of the Chomsky language hierarchy because the goal is always to create the simplest possible checker you can reliably show is able to accurately cover all the possible cases. Sometimes that is simple as a regular language, but the next rule might require you to have a parser for the language. For what it's worth, this is only one of the ways the guys at LaRS (http://lars-lab.jpl.nasa.gov/ http://lars-lab.jpl.nasa.gov/) help try to improve software reliability on-lab. Most of the members are world-class experts in formal verification analysis and try to integrate their knowledge with missions as effectively as possible. Sometimes, this means riding the dual responsibility of functioning as a researcher and a embedded flight software engineer, working alongside the rest of the team. If anyone's interested in trying out static analysis of C on your own, I highly reccomend checking out Eli Bendersky's awesome C parser for Python (http://code.google.com/p/pycparser/ http://code.google.com/p/pycparser/). I found it leaps and bounds better than the existing closed-source toolsets we had licenses for, like Coverity Extend. At the time, it had the extremely horrible limitation of only parsing ANSI 89, but Eli has since improved the parser to have ANSI 99 compliance. Analyzing C in Python is a dream.