[tooltower]

> [...] other algorithms may require the sort of induction one gets with constructive proofs to sufficiently verify. There is an art to this which will lead to style changes in C and a slightly different way of building up functions from pieces that can be trivially model checked.

Is there a book or article that talks more about this? I.e. how to write code in a way that is more amenable to model-checking (bounded or otherwise)?

[nanolith]

Unfortunately, I have not found any good tutorials. If it helps, I plan on writing one very soon.

[drdrey]

where can we follow you to hear more about this?