top | item 18997470 (no title) unboxed_type | 7 years ago Are you talking about CertiCoq project? It is not ready yet and not clear when will be.[1] https://www.cs.princeton.edu/~appel/certicoq/ discuss order hn newest nickpsecurity|7 years ago Talking about this: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.
nickpsecurity|7 years ago Talking about this: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.
nickpsecurity|7 years ago
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.