collaborators

1 paper

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…