|
|
|
|
|
|
by nickpsecurity
3257 days ago
|
|
|
I'm a fan of both sides of the Coq and Isabelle/HOL activities. I'm keeping an eye on CertiCoq. Right now, though, Isabelle/HOL seems to be ahead with work like Myreen and Davis's in terms of verified stacks: https://www.cl.cam.ac.uk/~mom22/ This data structure refinement with one version getting automated to a large degree: https://www21.in.tum.de/~lammich/pub/cpp2016_impds.pdf Thanks to DeepSpec, Coq might exceed that in some ways: https://deepspec.org/main Note that a lot of work around Coq goes through CompCert which is proprietary software with restrictions on how it's used if one doesn't pay. The Isabelle/HOL alternatives like Simpl/C and CakeML are free software. Then, outside those two, we got a bunch of work being done in Maude (esp K Framework) with one an executable, formal semantics for C done like a compiler: https://github.com/kframework/c-semantics |
|
|