Użytkownik "Waldek Hebisch" <a...@m...uni.wroc.pl> napisał:

> Z innej beczki, kilka lat temu zweryfikowano
> formalnie mikrojado L4.

Nie wierzę. C nie nadaje sie do weryfikacji formalnej poprawnosci programow
w nim pisanych (chyba ze jest to baaardzo okrojone C - i to o wiele bardziej niz
Misra C),
a jadro to jaderko na przyslowiowych "kilku kartkach" i "specjalnie pisane" pod
werfyfikację.

W zwyklym C/C++ formalna weryfikacja pooprawnosci to zwykla
uluda (i taka na zawsze zostanie).

AK


---
Ta wiadomość została sprawdzona na obecność wirusów przez oprogramowanie antywirusowe
Avast.
https://www.avast.com/antivirus