afv

AFV is an infinite state model checker that verifies iterative C programs by k-induction. AFV uses Yices as the backend SMT solver.