After my PhD, I worked in industry on the verification and development of software for a safety-critical environmental control system. The project used a variety of tools and processes to improve and demonstrate product quality. However, the only static analysis tool being used was lint. I thought there had to be something better.
As an intern at SQI I had worked one summer hacking Prolog to extend PASS-C, an extensible source code static analysis tool. However, most of the checks in that tool were about programming “style”. From academia, I knew that model checking had potential to support more powerful semantic checks. Model checking was increasingly being used for high-level system and hardware verification, but I wanted a software model checking tool for C and assembly source code.
The most promising tool I could find at the time was PREfast. Frustratingly, at the time I was looking, PREfast had been acquired by Microsoft to be used by them internally, and had been taken off the market! There was much gnashing of teeth. (Microsoft has more recently made it available again.) PREfast did deliver more powerful analyses, but it didn’t use model checking per se.
Now the tool I had been looking for is finally available: Goanna. It delivers many of the powerful and precise analyses I had dreamed of, and works for C, C++, and (unusually) embedded assembly. Goanna comes out of years of research and development at NICTA. It is packaged as an Eclipse plugin, and is available as a free trial.
Hi Mark, thanks for the post, additionally you’ll notice that I’ve announced our upcoming MSVS support http://www.redlizards.com/blog/?p=139 and we have an upcoming post regarding “Why Model Checking?” – very timely – thanks again, James.