Model Checking Embedded C Software Using k-Induction and Invariants
Raimundo da Silva Barreto
H. O. ROCHA
Lucas Carvalho Cordeiro