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