[SystemSafety] Scalability of Formal Methods [was: Logic]

[Derek M Jones]

Rod,

> 3) With compilers, you get what you pay for. Don't

This is not true.  What you get is roughly proportional
to what has been invested in writing and maintaining the compiler
over the years.

The problem with research on compiler quality (as measured by
probability of encountering a fault) is that the licensing terms
of commercial vendors don't allow test results for their products
to be published:
http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf

If anybody fancies testing their commercial compilers check out
Csmith:
http://embed.cs.utah.edu/csmith/

For other languages the basic principles are illustrated here:
http://shape-of-code.coding-guidelines.com/2011/04/25/simple-generator-for-compiler-stress-testing-source/

> confuse the quality of the "free" GCC builds from FSF, for example,
> with the quality of compilers from commercial vendors.

True. GCC is significantly better than most commercial compilers.

-- 
Derek M. Jones                  tel: +44 (0) 1252 520 667
Knowledge Software Ltd          blog:shape-of-code.coding-guidelines.com
Software analysis               http://www.knosof.co.uk