2 papers
cs.LO2015
Model Checking C Programs with Loops via k-Induction and Invariants
Herbert Rocha, Hussama Ismail, Lucas Cordeiro +1
We present a novel proof by induction algorithm, which combines k-induction with invariants to model check C programs with bounded and unbounded loops. The k-induction algorithm co…
cs.LO2011
Verifying Embedded C Software with Timing Constraints using an Untimed Model Checker
Raimundo Barreto, Lucas Cordeiro, Bernd Fischer
Embedded systems are everywhere, from home appliances to critical systems such as medical devices. They usually have associated timing constraints that need to be verified for the…