Model Checking Embedded C Software Using k-Induction and Invariants
Raimundo da Silva Barreto
HUSSAMA ISMAIL
HERBERT ROCHA