Rocha, Herbert, Hussama Ismail, Lucas Cordeiro, and Raimundo Barreto.
" Model Checking Embedded C Software Using k-Induction and Invariants." <em>Anais do V Simpósio Brasileiro de Engenharia de Sistemas Computacionais,
Foz do Iguaçu/PR, 2015</em>. SBC, 2015,  
pp.708-797.