[SystemSafety] Critical systems Linux

[David Crocker]

On 23/11/2018 18:01, Olwen Morgan wrote:
> ...It's a two-stage approach whereby (possibly draconian) subset
> checkers flag up usages that make life unnecessarily hard for proof
> tools and then the proof tools get to work on code that is, hopefully,
> more tractable to analyse.
Which is exactly what Escher C Verifier does (and other proof tools for
C AFAIK). The subset doesn't need to be draconian though, a subset of
the MISRA-C rules is more than adequate for this purpose.

OTOH for proofs in C++, the subset we support is is a much smaller
proportion of the whole language than it is for C. This is mostly
because some features of C++ are complex and don't always lend
themselves to design-by-contract, for example template specialisation.