Barreto, Raimundo, Lucas Cordeiro, and Bernd Fischer. " Verifying Embedded C Software with Timing Constraints Using an Untimed Bounded Model Checker." Anais do Simpósio Brasileiro de Engenharia de Sistemas Computacionais, Florianópolis, 2011. SBC, 2011, pp.46-52.