[Nokinside]

Astrée static analysis tool detects invalid pointer dereferences. It can give false alarms but it always detects errors. It does this buy using abstract interpretation on the semantics. It's essentially partial execution.