Re: [SystemSafety] Research topics

From: David Crocker < >
Date: Mon, 15 Jul 2013 19:06:21 +0100


Martin, we at Escher Technologies are in the process of doing much of what you suggested. We're defining a carefully-chosen subset of C++ that is type-safe and formally-verifiable, and we're extending Escher C Verifier to support it. The availability of C++ classes provides the encapsulation that is missing in C, while other features such as generics allow us to avoid many of the nastier features of C such as the way in which arrays are passed as parameters. We have a customer who has taken on the role of tame user.

I should stress that the C++ subset we are using is smaller than Misra C++ or JSF C++, because we have taken the approach that we will include only those constructs that are well-understood and useful to developers of critical embedded software, rather than start with the whole of C++ and then remove some features.

I would welcome input on the approach, and some more test users of the subset and tool when it is a little further advanced.

There are some short articles on formal verification of C/C++, together with some arguments about why I think a C++ subset is potentially safer to use than a C subset, on the Articles section of our web site.

Regards - David

Martyn Thomas <martyn_at_xxxxxx
>I attach a slightly modified Grand Challenge talk that I gave about 10
>years ago, based on a proposal that I had worked on with the help of
>Tony Hoare.
>
>Any significant progress towards this would be worth a PhD, in my
>opinion. Let me know if you decide to head down this path and if I can
>help ...
>
>Regards
>
>Martyn
>Martyn Thomas CBE FREng
>Vice President, Royal Academy of Engineering
>Chair, IT Policy Panel, Institution of Engineering and Technology
>
>On 15/07/2013 09:03, René Senden wrote:
>> Not necessarily, e.g. a research topic for a PhD research.
>
>
>
>------------------------------------------------------------------------
>
>_______________________________________________
>The System Safety Mailing List
>systemsafety_at_xxxxxx

-- 
Sent from my Android phone with K-9 Mail. Please excuse my brevity.



_______________________________________________ The System Safety Mailing List systemsafety_at_xxxxxx
Received on Mon Jul 15 2013 - 20:06:53 CEST

This archive was generated by hypermail 2.3.0 : Sun Feb 17 2019 - 08:17:05 CET