Copper

Copper is a software model checker that can be used to verify whether a concurrent C program satisfies its safety, reliability, or security requirements.