verdi icon indicating copy to clipboard operation
verdi copied to clipboard

Published 20 hours ago • verified publisher icon uwplse

Proposal: verify Verdi shim functions down to machine code

Open palmskog opened this issue 5 years ago • 0 comments

Several parts of the Verdi shims (currently based on OCaml) can be specified and verified down to machine code, for example using VST.

The current limitation is that there is no formal specification of UDP or TCP, which are used in the shims (all shims use TCP in some way).

palmskog avatar Oct 14 '19 13:10 palmskog