[SystemSafety] Critical systems Linux

[Olwen Morgan]

Any tool vendor claiming to do formal verification must, at least 
implicitly, be working to some kind of formal semantics. There may well 
be more than four formal definitions (of varying degrees of quality) 
lurking in the wide world.

Olwen

On 22/11/2018 13:48, Derek M Jones wrote:
> David,
>
>> While it's true that C doesn't have a formal semantics, in practice the
>> semantics of C is well-understood by experts, who write static analysis
>
> There are four formal definitions, that I am aware of, claiming to cover
> the complete C language.  None of them handle the preprocessor.
>
> At least one can be used to process and 'execute' C code.
>
>