Herbert Rocha, Hussama Ismail, Lucas Cordeiro, and Raimundo Barreto. 2015. Model Checking Embedded C Software Using k-Induction and Invariants. In Anais do V Simpósio Brasileiro de Engenharia de Sistemas Computacionais, novembro 03, 2015, Foz do Iguaçu/PR, Brasil. SBC, Porto Alegre, Brasil, 708-797.