search

google / zerocopy

https://discord.gg/MAvWH2R6zk
Apache License 2.0
1.58k stars 105 forks source link

Use formal modeling/verification to test or prove the correctness of core algorithms #378

Open joshlf opened 1 year ago

joshlf commented 1 year ago

While zerocopy is conceptually complex, the amount of code that executes in order to perform a particular operation is often very small. This makes it a perfect target for formal modeling and verification techniques.

This issue tracks testing or proving the correctness of our core algorithms using these tools.

Currently, we use formal modeling or verification in the following places (TODO: better way to keep this list up-to-date automatically?):

jswrenn commented 1 year ago

I left a comment about our need for alternative targets here: https://github.com/model-checking/kani/issues/2402#issuecomment-1726613332