[SystemSafety] Research topics

[David Crocker]

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 thomas-associates.co.uk> wrote:
>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 TechFak.Uni-Bielefeld.DE

-- 
Sent from my Android phone with K-9 Mail. Please excuse my brevity.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20130715/8a54259b/attachment.html>