Hacker News new | past | comments | ask | show | jobs | submit login

This article does not actually get anywhere with the "formal verification" part. The authors dumps it into a bounded model checker, observes that it does not work and then does some crude manual bounded loop unrolling. Does this increase confidence in the algorithm? Not sure.

Then you missed the point that CBMC is a formal verification tool (the best practical one btw), which also does bounded model checking. But it has of course its limitations, esp. with unbounded models, such as linked lists or recursion.

Here he explains how to overcome its limitations in one case. A likely bug in the loop unroller. With --unwind N you can tell CBMC how far to unroll automatically, and --depth is for recursion. In this case he just unrolled it manually. Note: should check if it works out of the box with a current version. CBMC is getting better and better lately.

I often use satabs then, which doesn't struggle with unbounded models, but has other limitations.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact