Re: [SystemSafety] Claims for formal methods

From: Derek M Jones < >
Date: Wed, 19 Feb 2014 10:59:51 +0000


> Now you seem to be abusing an entire community of researchers and
> engineers. Are you unable to put forward your beliefs more professionally?

I gave a succinct summary of my views.

> Please provide some examples (preferably from peer-reviewed journals) of
> the "excessive claims" that you are criticising.

There are the articles discussed in links I posted to the original thread:

The French group in the above links did some interesting work on compiler code generation and I believe they now refer to it as a verified compiler backend (which is what it idoes) rather than a verified C compiler.

For an impressive piece of work on creating a formal definition of a C compiler front end (syntax and semantics) supporting a substantial chunk of the C standard see:

> Then please explain how this provides enough evidence for accusing a
> whole community of a "culture of intellectual dishonesty".

Thanks, but I am content to sit in my corner of the world and leave the entrenched positions be.

> Martyn
> On 19/02/2014 00:16, Derek M Jones wrote:
>> The current culture of intellectual dishonesty in the formal methods
>> community is switching off interest from potential users.
>> Justifying excessive claims by using weasel words to show how
>> wording can be interpreted to reflect reality is not the way to
>> convince people to try something new.
>> Researchers should ask themselves whether their paper would stand
>> scrutiny from the advertising standards authority.
>> Soap power manufacturers have their claims scrutinized and I think
>> we all agree that claims made about the use of formal methods should
>> also meet this minimum requirement.
> _______________________________________________
> The System Safety Mailing List
> systemsafety_at_xxxxxx >

Derek M. Jones                  tel: +44 (0) 1252 520 667
Knowledge Software Ltd
Software analysis     
The System Safety Mailing List
Received on Wed Feb 19 2014 - 12:00:31 CET

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