Mikrojádro seL4 je matematicky verifikováno pro architekturu RISC-V
Organizace RISC-V Foundation oznámila verifikaci mikrokerneru seL4 na systémech s architekturou RISC-V. Verifikace spočívá v matematickém důkazu spolehlivosti provozu seL4, což potvrzuje plnou shodu s požadavky specifikovanými formálním jazykem. Důkaz spolehlivosti umožňuje použití seL4 v kritických systémech založených na procesorech RISC-V RV64, které vyžadují zvýšenou úroveň spolehlivosti a zaručují absenci […]
