> in my trivial example if the accumulator (C_n) at the maximum value, it would overflow for any non-zero input Depends on what you mean by "incorrect". :) Th

> in my trivial example if the accumulator (C_n) at the maximum value, it would overflow for any non-zero input Depends on what you mean by "incorrect". :) The SMT formulation isn't doing infinite precision arithmetic. It's just proving that the result computed by (the SMT encoding of) the C macro is equivalent to the 64-bit SMT bitvector defined by "Concat(c2, c1, c0) + 2 * ZeroExt(2W, a) ZeroExt(2W, b)". > A lot of effort, to prove very narrow properties-- ones which might be misleading about the correctness of the software, on models which may not well match the actual software, and which gives assurance that rots a bit over time because it's not sufficiently automatic.* To some extent, I agree with you. It is a little difficult to find off-the-shelf tools that work well directly on the source code, especially for software. But I think it's a just a matter of time before these issues are resolved. The hardware scenario has certainly improved in leaps and bounds. A group I've worked with has been somewhat successful in pushing the use of the JasperGold model checker at Intel, and I've heard quite a few people with no background in using formal tools tell me that they're happy with the tool and are much more confident in their code thanks to use of this tool.