4 ms·
CompCert, CakeML, Simpl/C, VeLLVM, and SPARK Ada are the related reading for those interested in this sort of thing. The others naturally fit the topic with SPA
by nickpsecurity 9y ago
CompCert, CakeML, Simpl/C, VeLLVM, and SPARK Ada are the related reading for those interested in this sort of thing. The others naturally fit the topic with SPARK being a mature tool for verifying imperative algorithms.