[1] https://www.cs.princeton.edu/~appel/certicoq/
https://staff.aist.go.jp/tanaka-akira/succinct/slide-pro114....
They extract from Coq to C. Like in my Brute-Force Assurance concept, that would let us confirm and supplement the formal verification by hitting the C output with every V&V tool for C programs that we have on hand.
https://staff.aist.go.jp/tanaka-akira/succinct/slide-pro114....
They extract from Coq to C. Like in my Brute-Force Assurance concept, that would let us confirm and supplement the formal verification by hitting the C output with every V&V tool for C programs that we have on hand.