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

From: Derek M Jones < >
Date: Thu, 27 Feb 2014 13:28:10 +0000


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
_______________________________________________
The System Safety Mailing List
systemsafety_at_xxxxxx
Received on Thu Feb 27 2014 - 14:28:42 CET

This archive was generated by hypermail 2.3.0 : Tue Jun 04 2019 - 21:17:06 CEST