Here is a challenge for people who are interested in practical C program verification using formal methods. Show us how to verify the correctness of the twenty-five programs in the paper A benchmark for C program verification.

If you are interested in this in any way, feel free to send me mail (and preferably verification proofs of these programs) at [email protected].