This is a code analysis tool for C programs that can check for interesting security properties using a "model checking" approach. The current tool is a research-oriented tool that doesn't contain a significant database of knowledge, but that is expected to change eventually. If something in its database, it does a much better analysis than tools like RATS in that it has far fewer false positives.
There are some kinds of security problems that aren't well-suited for analysis by this model checking approach, such as buffer overflow and integer signedness problems. Other analysis tools help address these problems.
![[Python Powered]](images/PythonPoweredSmall.gif)
