This short presentation shows Frama-C and CBMC at work and tackling some few little infinite loops.